共查询到20条相似文献,搜索用时 15 毫秒
1.
This paper investigates the feasibility of reducing a model-checking problem K??? ? for discrete time Duration Calculus to the decision problem for Presburger Arithmetic. Theoretical results point at severe limitations of this approach: (1) the reduction in Fränzle and Hansen (Int J Softw Inform 3(2–3):171–196, 2009) produces Presburger formulas whose sizes grow exponentially in the chop-depth of ?, where chop is an interval modality originating from Moszkowski (IEEE Comput 18(2):10–19, 1985), and (2) the decision problem for Presburger Arithmetic has a double exponential lower bound and a triple exponential upper bound. The generated Presburger formulas have a rich Boolean structure, many quantifiers and quantifier alternations. Such formulas are simplified using so-called guarded formulas, where a guard provides a context used to simplify the rest of the formula. A normal form for guarded formulas supports global effects of local simplifications. Combined with quantifier-elimination techniques, this normalization gives significant reductions in formula sizes and in the number of quantifiers. As an example, we solve a configuration problem using the SMT-solver Z3 as backend. Benefits and the current limits of the approach are illustrated by a family of examples. 相似文献
2.
We present a logic which we call Hybrid Duration Calculus (HDC). HDC is obtained by adding the following hybrid logical machinery to the Restricted Duration Calculus (RDC): nominals, satisfaction operators, down-arrow binder, and the global modality. RDC is known to be decidable, and in this paper we show that decidability is retained when adding the hybrid logical machinery. Decidability of HDC is shown by reducing the satisfiability problem to satisfiability of Monadic Second-Order Theory of Order. We illustrate the increased expressive power obtained in hybridizing RDC by showing that HDC, in contrast to RDC, can express all of the 13 possible relations between intervals. 相似文献
3.
Since the seminal work of Zhou Chaochen, M. R. Hansen, and P. Sestoft on decidability of dense-time Duration Calculus [ZHS93] it is well known that decidable fragments of Duration Calculus can only be obtained through withdrawal of much of the interesting vocabulary of this logic. While this was formerly taken as an indication that key-press verification of implementations with respect to elaborate Duration Calculus specifications were also impossible, we show that the model property is well decidable for realistic designs which feature natural constraints on their switching dynamics.The key issue is that the classical undecidability results rely on a notion of validity of a formula that refers to a class of models which is considerably richer than the possible behaviours of actual embedded real-time systems: that of finitely variable trajectories. By analysing two suitably sparser model classes we obtain model-checking procedures for rich subsets of Duration Calculus. Together with undecidability results also obtained, this sheds light upon the exact borderline between decidability and undecidability of Duration Calculi and related logics.Received June 1999Accepted in revised form September 2003 by M. R. Hansen and C. B. Jones 相似文献
5.
TheDurationCalculus(abbreviatedDC)representsalogicalapproachtoformaldesignofreal-timesystems.DCisbasedonintervallOgic,andusestherealnumberstomodeltime,andBoolean-valued(i.e.{0,1}-valued)functionsovertimetomodelstatesandeventsofreaLtimesystems.Thedurationofastateinatimeintervalistheaccumulatedpresencetimeofthestateintheinterval.DCextendsintervallogicwithacalculustospecifyandreasonaboutpropertiesofstatedurations.TheresearchofDCwasintroducedintheProCoSproject(ESPRITBRA3104and7071),whent… 相似文献
6.
This paper compares the expressive power of first-order monadic logic of order, a fundamental formalism in mathematical logic and the theory of computation, with that of the propositional version of duration calculus (PDC), a formalism for the specification of real-time systems. Our results show that the propositional duration calculus is expressively complete for first-order monadic logic of order. Our semantics for PDC conservatively extends the standard semantics to all positive (including infinite) length intervals. Hence, in view of the expressive completeness, liveness properties can be specified in PDC. This observation refutes a widely believed misconception that the duration calculus cannot specify liveness properties. 相似文献
7.
This paper deals with dependability of imperfect implementations concerning given requirements. The requirements are assumed
to be written as formulas in Duration Calculus. Implementations are modelled by continuous semi-Markov processes with finite
state space, which are expressed in the paper as finite automata with stochastic delays of state transitions. A probabilistic
model for Duration Calculus formulas is introduced, so that the satisfaction probabilities of Duration Calculus formulas with
respect to semi-Markov processes can be defined, reasoned about and calculated through a set of axioms and rules of the model.
Received November 1994 / Accepted in revised form June 1998 相似文献
8.
Current practices in the verification of commercial hardware designs (digital, synchronous, and sequential semiconductors)
are described. Recent advances in verification by the mathematical technique called model checking are described, and requirements
for the successful application of model checking in commercial design are discussed. 相似文献
9.
在Pandya提出的CTL*[DC]逻辑的基础上,对其语法和语义进行扩展,并对路径长度进行限制,定义了一个新的逻辑CTL*[k-QDDC],它可应用于实时系统的描述和验证.给出了在Kripke结构中直接验证CTL*[k-QDDC]逻辑公式在某状态是否成真的基本算法.在某些假设下,也证明了CTL*[k-QDDC]中的某个逻辑运算符的验证问题是NP完全的,这就说明CTL*[k-QDDC]的验证问题至少是NP难的. 相似文献
10.
时段演算是描述和推导嵌入式实时系统和混成系统性质的一种区间时态逻辑.扩展线性时段不变式是时段演算的重要子集.针对实时自动机,提出一种连续时间语义下扩展线性时段不变式的有界模型检验方法.该方法将扩展线性时段不变式的有界模型检验问题转化为量词线性算术公式的正确性问题,从而可以采用量词消去技术进行求解.首先,运用符号化的思想,在实时自动机上利用深度优先搜索找到所有满足观测时长约束的符号化路径片段;然后,将每条符号化路径片段转化为一个量词线性算术公式;最后,利用量词消去工具求解.与已有工作相比,基于实时自动机设计了验证算法.另外,降低了验证复杂度,并且加速了验证过程的实际速度. 相似文献
11.
The goal of this paper is to translate (fragments of) the quantified discrete duration calculus QDDC, proposed by P. Pandya, into symbolic acceptors with counters. Acceptors are written in the synchronous programming language Lustre, in order to allow available symbolic verification tools (model-checkers, abstract interpreters) to be applied to properties expressed in QDDC. We show that important constructs of QDDC need non-deterministic acceptors, in order to be translated with a bounded number of counters, and an expressive fragment of the logic is identified and translated. Then, we consider a more restricted fragment, which only needs deterministic acceptors. 相似文献
12.
The Shape Calculus is a spatio-temporal logic based on an n-dimensional Duration Calculus tailored for the specification and verification of mobile real-time systems. After showing non-axiomatisability, we give a complete embedding in n-dimensional interval temporal logic and present two different decidable subsets, which are important for tool support and practical use. 相似文献
13.
We study a new operator of projection onto state and the prefix operator in the extension μ HDC of DC by quantifiers over state and a polyadic least fixed point operator. We give axioms and rules to enable deduction in the extension of μ HDC by the new operators. Our axioms can be used to eliminate the new operators from formulas in a practically significant fragment of μ HDC. This entails the decidability of certain subfragments of this fragment is preserved in the presence of the new operators. 相似文献
14.
Abstract Abstract. This article is concerned with methods and experiences in usability testing of standard application business software. In order to achieve the multiple trade-off between scientific objectivity, practical applicability, and the cost-benefit ratio, a set of standard methods and the resulting testing environment in the ergonomics lab are described and demonstrated by examples. Stumbling blocks are discussed. Necessary additional prerequisites for a successful practical approach are stressed. 相似文献
15.
In this paper we present efficient symbolic techniques for probabilistic model checking. These have been implemented in PRISM, a tool for the analysis of probabilistic models such as discrete-time Markov chains, continuous-time Markov chains and Markov decision processes using specifications in the probabilistic temporal logics PCTL and CSL. Motivated by the success of model checkers such as SMV which use BDDs (binary decision diagrams), we have developed an implementation of PCTL and CSL model checking based on MTBDDs (multi-terminal BDDs) and BDDs. Existing work in this direction has been hindered by the generally poor performance of MTBDD-based numerical computation, which is often substantially slower than explicit methods using sparse matrices. The focus of this paper is a novel hybrid technique which combines aspects of symbolic and explicit approaches to overcome these performance problems. For typical examples, we achieve a dramatic improvement over the purely symbolic approach. In addition, thanks to the compact model representation using MTBDDs, we can verify systems an order of magnitude larger than with sparse matrices, while almost matching or even beating them for speed. 相似文献
17.
使用扩展的持续时间演算(EDC)模型,给出了时间化的RAISE描述语言(RSL)的一个子集的指称语义.在扩展的持续时间演算模型中加入了一些新的特征,并探究了它们的代数定律.这些定律在形式化实时程序和验证实时性质中起着重要作用.最后还给出了时间化RSL的一些代数定律.这些定律可以从其指称语义证明,并用于程序的转化和优化. 相似文献
18.
The notion of contract was introduced to component-based software development in order to facilitate the semantically correct composition of components. We extend the form of this notion which is based on designs to capture probabilistic requirements on execution time. We show how reasoning about such requirements can be done in an infinite-interval-based system of probabilistic duration calculus. 相似文献
19.
Regular model checking is the name of a family of techniques for analyzing infinite-state systems in which states are represented by words, sets of states by finite automata, and transitions by finite-state transducers. In this framework, the central problem is to compute the transitive closure of a transducer. Such a representation allows to compute the set of reachable states of the system and to detect loops between states. A main obstacle of this approach is that there exists many systems for which the reachable set of states is not regular. Recently, regular model checking has been extended to systems with tree-like architectures. In this paper, we provide a procedure, based on a new implementable acceleration technique, for computing the transitive closure of a tree transducer. The procedure consists of incrementally adding new transitions while merging states, which are related according to a pre-defined equivalence relation. The equivalence is induced by a downward and an upward simulation relation, which can be efficiently computed. Our technique can also be used to compute the set of reachable states without computing the transitive closure. We have implemented and applied our technique to various protocols. 相似文献
20.
Model checking (Baier and Katoen in Principles of model checking, MIT Press, Cambridge, 2008; Clarke et al. in Model checking, MIT Press, Cambridge, 2001) is an automatic technique to formally verify that a given specification of a concurrent system meets given functional properties. Its use has been demonstrated many times over the years. Key characteristics that make the method so appealing are its level of automaticity, its ability to determine the absence of errors in the system (contrary to testing techniques) and the fact that it produces counter-examples when errors are detected, that clearly demonstrate not only that an error is present, but also how the error can be produced. The main drawback of model checking is its limited scalability, and for this reason, research on reducing the computational effort has received much attention over the last decades. Besides the verification of qualitative functional properties, the model checking technique can also be applied for other types of analyses, such as planning and the verification of quantitative properties. We briefly discuss several contributions in the model checking field that address both its scalability and its applicability to perform planning and quantitative analysis. In particular, we introduce six papers selected from the 23rd International SPIN Symposium on Model Checking Software (SPIN 2016). 相似文献
|