Models and temporal logical specifications for timed component connectors

Component-based software engineering advocates construction of software systems through composition of coordinated autonomous components. Significant benefits of this approach include software reuse, simpler and faster construction, enhanced reliability, and dramatic reductions in the complexity of construction of provably correct critical systems, many of which involve real-time concerns. Effective, flexible component composition by itself still poses a challenge today and yet the special nature of real-time constraints makes component-based construction of real-time systems even more demanding. The coordination language Reo supports compositional system construction through connectors that exogenously coordinate the interactions among the constituent components which unawarely comprise a complex system, into a coherent collaboration. The simple, yet surprisingly rich, calculus of channel composition that underlies Reo offers a flexible framework for compositional construction of coordinating component connectors with real-time properties. In this paper, we present an operational semantics for the channel-based component connectors of Reo in terms of Timed Constraint Automata and introduce a temporal-logic for specification and verification of their real-time properties.      

Symbolic Model Checking for Channel-based Component Connectors

The paper reports on the foundations and experimental results with a model checker for component connectors modelled by networks of channels in the calculus Reo. The specification formalisms is a branching time logic that allows to reason about the coordination principles of and the data flow in the network. The underlying model checking algorithm relies on variants of standard automata-based approaches and model checking for CTL-like logics. The implementation uses a symbolic representation of the network and the enabled I/O-operations by means of binary decision diagrams. It has been applied to a couple examples that illustrate the efficiency of our model checker.     

Probabilistic symbolic model checking with PRISM: a hybrid approach

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.     

Automatic software model checking via constraint logic

This paper proposes the use of constraint logic to perform model checking of imperative, infinite-state programs. We present a semantics-preserving translation from an imperative language with recursive procedures and heap-allocated mutable data structures into constraint logic. The constraint logic formulation provides a clean way to reason about the behavior and correctness of the original program. In addition, it enables the use of existing constraint logic implementations to perform bounded software model checking, using a combination of symbolic reasoning and explicit path exploration.     

Test sequence generation and model checking using dynamic transition relations

The task of finding a set of test sequences that provides good coverage of industrial circuits is infeasible because of the size of the circuits. For small critical subcircuits of the design, however, designers can create a set of test sequences that achieve good coverage. These sequences cannot be used on the full design because the inputs to the subcircuit may not be accessible. In this work we present an efficient test generation algorithm that receives a test sequence created for the subcircuit and finds a test sequence for the full design that reproduces the given sequence on the subcircuit. The algorithm uses a new technique called dynamic transition relations to increase its efficiency .The most common and most expensive step in our algorithm is the computation of the set of predecessors of a set of states. To make this computation more efficient we exploit a partitioning of the transition relation into a set of simpler relations. At every step we use only those that are necessary, resulting in a smaller relation than the original one. A different relation is used for each step, hence the name dynamic transition relations. The same idea can be used to improve symbolic model checking for the temporal logic CTL.We have implemented the new method in SMV and run it on several large circuits. Our experiments indicate that the new method can provide gains of up to two orders of magnitude in time and space during verification. These results show that dynamic transition relations can make it possible to verify circuits that were previously unmanageable due to their size and complexity .     

Assumption-based distribution of CTL model checking

In this paper we discuss the problem of performing distributed CTL model checking by splitting the given state space into several partial state spaces. The partial state space is modelled as a Kripke structure with border states. Each computer involved in the distributed computation owns a partial state space and performs a model-checking algorithm on this incomplete structure. To be able to proceed, the border states are augmented by assumptions about truth values of formulas and the computers exchange assumptions about relevant states to compute more precise information.     

Model checking LTL with regular valuations for pushdown systems

Recent works have proposed pushdown systems as a tool for analyzing programs with (recursive) procedures, and the model-checking problem for LTL has received special attention. However, all these works impose a strong restriction on the possible valuations of atomic propositions: whether a configuration of the pushdown system satisfies an atomic proposition or not can only depend on the current control state of the pushdown automaton and on its topmost stack symbol. In this paper we consider LTL with regular valuations: the set of configurations satisfying an atomic proposition can be an arbitrary regular language. The model-checking problem is solved via two different techniques, with an eye on efficiency. The resulting algorithms are polynomial in certain measures of the problem which are usually small, but can be exponential in the size of the problem instance. However, we show that this exponential blowup is inevitable. The extension to regular valuations allows to model problems in different areas; for instance, we show an application to the analysis of systems with checkpoints. We claim that our model-checking algorithms provide a general, unifying and efficient framework for solving them.     

Symbolic abstraction and deadlock-freeness verification of inter-enterprise processes

The design of complex inter-enterprise business processes (IEBP) is generally performed in a modular way. Each process is designed separately and then the whole IEBP is obtained by composition. Even if such a modular approach is intuitive and facilitates the design problem, it poses the problem that correct behavior of each business process of the IEBP taken alone does not guarantee a correct behavior of the composed IEBP (i.e. properties are not preserved by composition). Proving correctness of the (unknown) composed process is strongly related to the model checking problem of a system model. Among others, the symbolic observation graph based approach has proven to be very helpful for efficient model checking in general. Since it is heavily based on abstraction techniques and thus hides detailed information about system components that are not relevant for the correctness decision, it is promising to transfer this concept to the problem raised in this paper: How can the symbolic observation graph technique be adapted and employed for process composition? Answering this question is the aim of this paper.     

On model checking multiple hybrid views

Many applications, for instance the MS .NET Global Assembly Cache (GAC), are naturally expressed as 3-valued models where an additional third truth value models uncertainty or under-specification. An example of under-specification is that a component in a GAC may or may not have a main method. Models described in this manner can then be analyzed to refute or verify properties about the concrete systems they intend to model. This approach to system validation traditionally considers only one model at a time, even though this model may evolve if subjected to analysis. Many applications, however, benefit from or require the simultaneous consideration of multiple models of systems. We mention here requirements from different stake holders, and data drawn from federated databases.     

时间自动机的LTL性质模型检测研究

为了增强模型检测工具的检测能力,拓宽模型检测技术的应用范围,对基于时间自动机的LTL性质模型检测进行了研究,对自动机的状态空间的存储方式和状态空间的展开过程进行了分析,讨论了LTL性质模型检测工具的检测流程和检测算法的实现策略对工具检测性能的影响,针对制约模型工具的检测能力和检测效率的因素,采取了一些相应的优化改进策略.采用了BDD(二叉决策图)共享存储技术和位编码压缩存储,较有效地减小了空间消耗,缓解了模型检测中状态爆炸引起的内存空间不足问题.与DTSpin等著名的模型检测工具进行了实验比较,取得了较好的实验结果.     

On the use of MTBDDs for performability analysis and verification of stochastic systems

This paper describes how to employ multi-terminal binary decision diagrams (MTBDDs) for the construction and analysis of a general class of models that exhibit stochastic, probabilistic and non-deterministic behaviour. It is shown how the notorious problem of state space explosion can be circumvented by compositionally constructing symbolic (i.e. MTBDD-based) representations of complex systems from small-scale components. We emphasise, however, that compactness of the representation can only be achieved if heuristics are applied with insight into the structure of the system under investigation. We report on our experiences concerning compact representation, performance analysis and verification of performability properties.     

符号化模型检测CTL

提出了一个关于时态逻辑CTL＊ 的符号化模型检测算法.该算法通过所谓的tableau构造方法来判定一个有限状态系统是否满足CTL＊规范. 根据该理论,作者已实现了一个基于OBDD技术的CTL＊符号化模型检测工具MCTK,并完成了相当数量的实验.到目前为止,已知有名的符号化模型检测工具,如SMV和NuSMV等, 都只能对CTL＊的子集逻辑（如CTL,LTL）进行检测,而文中算法的结果是令人满意的,并且当规范不是特别复杂时, 高效的CTL＊符号化模型检测是可能的.     

Some current topics in model checking

Model checking is a particular approach to property verification of systems. One describes a system in a mathematical model, expresses the properties one wishes to verify for the system in a formal language, and then checks whether the model satisfies the formal property. Invented 25 years ago, this approach is fully automatic and has therefore gained wide acceptance and is increasingly being used in commercial research and development units. Impediments remain on the road to successful technology transfer. For one, the size of models often increases exponentially in the number of variables or sub-models, preventing scalable automation. Abstracting a model to reduce its size can be a cost-effective way of addressing this. For another, systems and models may be subject to change, e.g. in an incremental design process. One then seeks cost-effective means of ascertaining that property verifications remain to be valid as models evolve. This special section presents current research on such abstraction and change management of model checking.     

Efficient reduction of finite state model checking to reachability analysis

Two types of temporal properties are usually distinguished: safety and liveness. Recently we have shown how to verify liveness properties of finite state systems using safety checking. In this article we extend the translation scheme to typical combinations of temporal operators. We discuss optimizations that limit the overhead of our translation. Using the notions of predicated diameter and radius we obtain revised bounds for our translation scheme. These notions also give a tight bound on the minimal completeness bound for simple liveness properties. Experimental results show the feasibility of the approach for complex examples. For one example, even an exponential speedup can be observed.     

Generating BDDs for symbolic model checking in CCS

Summary Finite transition systems can easily be represented by binary decision diagrams (BDDs) through the characteristic function of the transition relation. Burch et al. have shown how model checking of a powerful version of the -calculus can be performed on such BDDs. In this paper we show how a BDD can be generated from elementary finite transition systems given as BDDs by applying the CCS operations of parallel composition, restriction, and relabelling. The resulting BDDs only grow linearly in the number of parallel components. This way bisimilarity checking can be performed for processes out of the reach of conventional process algebra tools. Reinhard Enders graduated from the Technical University in Munich with a Diploma in mathematics and computer science in 1978. From 1977 to 1984 he was employed by Siemens, working in computer linguistics and expert systems. From 1984 to 1988 he worked at ECRC on Prolog extensions. In Autmn 1988 he joined Siemens and is developping the constraint extension of a new Prolog product. Thomas Filkorn received the computer science degree and the Ph.D. degree, both from the Technical University of Munich. Since 1992 he works at Siemens' Corporate Research and Development on symbolic algorithms and methods for the verification of finite state systems. Dirk Taubner received his Ph.D. in informatics at the Technical University of Munich in 1988. He investigated which sublanguages of process algebra could be represented finitely by automata and Petri nets. From 1989 through 91 he worked at Siemens' Corporate Research and Development where he led a project on computer-aided verification of parallel processes. This paper presents part of the work of that project. Currently he works on commercial software engineering for a software consulting company.     

Scaling model checking of dataraces using dynamic information

Dataraces in multithreaded programs often indicate severe bugs and can cause unexpected behaviors when different thread interleavings are executed. Because dataraces are a cause for concern, many works have dealt with the problem of detecting them. Works based on dynamic techniques either report errors only for dataraces that occur in the current interleaving, which limits their usefulness, or produce many spurious dataraces. Works based on model checking search exhaustively for dataraces and thus can reveal even those that occur in rarely executed paths. However, the applicability of model checking is limited because the large number of thread interleavings in realistic multithreaded programs causes state space explosion. In this work, we combine the two techniques in a hybrid scheme which overcomes these difficulties and enjoys the advantages of both worlds. Our hybrid technique succeeds in providing thread interleavings that prove the existence of dataraces in realistic programs. The programs we experimented with cannot be checked using either an ordinary industrial strength model checker or bounded model checking.     

Analysing a stream authentication protocol using model checking

In this paper, we consider how one can analyse a stream authentication protocol using model checking techniques. In particular, we will be focusing on the Timed Efficient Stream Loss-tolerant Authentication Protocol, TESLA. This protocol differs from the standard class of authentication protocols previously analysed using model checking techniques in the following interesting way: an unbounded stream of messages is broadcast by a sender, making use of an unbounded stream of keys; the authentication of the n-th message in the stream is achieved on receipt of the n+1-th message. We show that, despite the infinite nature of the protocol, it is possible to build a finite model that correctly captures its behaviour.     

基于Yices对时间自动机的有界模型检测

为了避免在有界模型检测过程中对变量进行布尔编码以及对时间自动机模型中的时钟进行预处理,给出一个利用SMT(satisfiability modulo theories)工具进行的对时间自动机进行有界模型检测的方法.该方法将时间自动机模型直接转换成SMT工具可识别的逻辑公式,利用SMT工具可求解包含有整数型和实数型变量逻辑公式的能力来进行模型检测.实验结果表明,对于某些可达性性质的验证,该方法的效率有一定的优势.     

Symbolic Graphs: Linear Solutions to Connectivity Related Problems

The importance of symbolic data structures such as Ordered Binary Decision Diagrams (OBDD) is rapidly growing in many areas of Computer Science where the large dimensions of the input models is a challenging feature: OBDD based graph representations allowed to define truly new standards in the achievable dimensions for the Model Checking verification technique. However, OBDD representations pose strict constraints in the algorithm design issue. For example, Depth-First Search (DFS) is not feasible in a symbolic framework and, consequently, many state-of-the-art DFS based algorithms (e.g., connectivity procedures) cannot be easily rearranged to work on symbolically represented graphs. We devise here a symbolic algorithmic strategy, based on the new notion of spine-set, that is general enough to be the engine of linear symbolic step algorithms for both strongly connected components and biconnected components. Our procedures improve on previously designed connectivity symbolic algorithms. Moreover, by an application to the so-called “bad cycle detection problem”, our technique can be used to efficiently solve the emptiness problem for various kinds of ω-automata. This work is a revised and extended version of [22,23]. It is partially supported by the projects PRIN 2005015491 and BIOCHECK.