Verification of clocked and hybrid systems

This paper presents a new computational model for real-time systems, called the clocked transition system (CTS) model. The CTS model is a development of our previous timed transition model, where some of the changes are inspired by the model of timed automata. The new model leads to a simpler style of temporal specification and verification, requiring no extension of the temporal language. We present verification rules for proving safety a nd liveness properties of clocked transition systems. All rules are associated with verification diagrams. The verification of response properties requires adjustments of the proof rules developed for untimed systems, reflecting the fact that progress in the real time systems is ensured by the progress of time and not by fairness. The style of the verification rules is very close to the verification style of untimed systems which allows the (re)use of verification methods and tools, developed for u ntimed reactive systems, for proving all interesting properties of real-time systems. We conclude with the presentation of a branching-time based approach for verifying that an arbitrary given CTS isnon-zeno. Finally, we present an extension of the model and the invariance proof rule for hybrid systems. Received: 23 September 1998 / 7 June 1999     

Termination Criteria for Bounded Model Checking: Extensions and Comparison

Increasing attention has been paid recently to criteria that allow one to conclude that a structure models a linear-time property from the knowledge that no counterexamples exist up to a certain length. These termination criteria effectively turn Bounded Model Checking into a full-fledged verification technique and sometimes result in considerable time savings. In [M. Awedh and F. Somenzi. Proving more properties with bounded model checking. In R. Alur and D. Peled, editors, Sixteenth Conference on Computer Aided Verification (CAV'04), pages 96–108. Springer-Verlag, Berlin, July 2004. LNCS 3114] we presented a criterion based on the translation of the linear-time specification into a Büchi automaton. BMC can be terminated if no fair cycle is found up to a given length, and one can prove that no fair cycle exists beyond that length. The maximum length for which counterexamples are explicitly checked is called the termination length; it obviously depends on the model, the property, and the termination criterion. In this paper we improve the criterion of [M. Awedh and F. Somenzi. Proving more properties with bounded model checking. In R. Alur and D. Peled, editors, Sixteenth Conference on Computer Aided Verification (CAV'04), pages 96–108. Springer-Verlag, Berlin, July 2004. LNCS 3114] by adding a check that often substantially reduces termination length. Our previous work employed translation to a non-generalized Büchi automaton. Though a well-known technique converts a generalized automaton into that form by composing it with a counter, it has the undesirable effect of considerably lengthening the cycles in the graph to be searched. We propose several alternatives to that approach and compare them experimentally. The translation to automata can be accomplished in more than one way, and in this paper we contrast two of them: one based on the algorithms of [F. Somenzi and R. Bloem. Efficient Büchi automata from LTL formulae. In E. A. Emerson and A. P. Sistla, editors, Twelfth Conference on Computer Aided Verification (CAV'00), pages 248–263. Springer-Verlag, Berlin, July 2000. LNCS 1855], and one based on the notion of tight automaton of [E. Clarke, O. Grumberg, and K. Hamaguchi. Another look at LTL model checking. In D. L. Dill, editor, Sixth Conference on Computer Aided Verification (CAV'94), pages 415–427. Springer-Verlag, Berlin, 1994. LNCS 818]. The latter yields shorter counterexamples, but the former often leads to earlier termination. In addition, it can help in identifying safety properties, for which termination checks are much more efficient than for the general case. We finally present results on comparing techniques based on cycle detection to the technique of [V. Schuppan and A. Biere. Efficient reduction of finite state model checking to reachability analysis. Software Tools for Technology Transfer, 5(2–3):185–204, Mar. 2004], which converts liveness properties into safety properties by augmentation of the model.     

A process algebraic framework for specification and validation of real-time systems

Following the trend to combine techniques to cover several facets of the development of modern systems, an integration of Z and CSP, called Circus, has been proposed as a refinement language; its relational model, based on the unifying theories of programming (UTP), justifies refinement in the context of both Z and CSP. In this paper, we introduce Circus Time, a timed extension of Circus, and present a new UTP time theory, which we use to give semantics to Circus Time and to validate some of its laws. In addition, we provide a framework for validation of timed programs based on FDR, the CSP model-checker. In this technique, a syntactic transformation strategy is used to split a timed program into two parallel components: an untimed program that uses timer events, and a collection of timers. We show that, with the timer events, it is possible to reason about time properties in the untimed language, and so, using FDR. Soundness is established using a Galois connection between the untimed UTP theory of Circus (and CSP) and our time theory.     

Delay-robustness in distributed control of timed discrete-event systems based on supervisor localisation

Recently, we studied communication delay in distributed control of untimed discrete-event systems based on supervisor localisation. We proposed a property called delay-robustness: the overall system behaviour controlled by distributed controllers with communication delay is logically equivalent to its delay-free counterpart. In this paper, we extend our previous work to timed discrete-event systems, in which communication delays are counted by a special clock event tick. First, we propose a timed channel model and define timed delay-robustness; for the latter, a verification procedure is presented. Next, if the delay-robust property does not hold, we introduce bounded delay-robustness, and present an algorithm to compute the maximal delay bound (measured by number of ticks) for transmitting a channelled event. Finally, we demonstrate delay-robustness on the example of an under-load tap-changing transformer.     

On a simplified untiming procedure for supervisory control of timed automata when the time increases strictly monotonically

Given a timed automaton G accepting the timed language L ^T a finite state machine G′ can be constructed, known as the region automaton, which accepts the untimed language Untime (L ^T). In this paper we construct an alternative finite state machine which also accepts the language Untime (L ^T), but has fewer states than G′. This is shown for languages of both finite and infinite traces given that the time values in the time sequence increase strictly monotonically. The supervisory control design for timed automata, when the simplified untiming procedure is used and the time is strictly positive, is studied.     

TCTL Inevitability Analysis of Dense-Time Systems: From Theory to Engineering

Inevitability properties in branching temporal logics are of the syntax foralldiamondsuit phi, where phi is an arbitrary (timed) CTL (Computation Tree Logic) formula. Such inevitability properties in dense-time logics can be analyzed with the greatest fixpoint calculation. We present algorithms to model-check inevitability properties. We discuss a technique for early decision on greatest fixpoint calculation which has shown promising performance against several benchmarks. We have experimented with various issues which may affect the performance of TCTL inevitability analysis. Specifically, our algorithms come with a parameter for the measurement of time-progress. We report the performance of our implementation with regard to various parameter values and with or without the non-Zeno computation requirement in the evaluation of greatest fixpoints. We have also experimented with safe abstraction techniques for model-checking TCTL inevitability properties. The experiment results help us in deducing rules for setting the parameter for verification performance. Finally, we summarize suggestions for configurations of efficient TCTL inevitability evaluation procedure.     

Automatic Verification of the IEEE-1394 Root Contention Protocol with KRONOS and PRISM

We report on the automatic verification of timed probabilistic properties of the IEEE 1394 root contention protocol combining two existing tools: the real-time model-checker KRONOS and the probabilistic model-checker PRISM. The system is modelled as a probabilistic timed automaton. We first use KRONOS to perform a symbolic forward reachability analysis to generate the set of states that are reachable with non-zero probability from the initial state, and before the deadline expires. We then encode this information as a Markov decision process to be analyzed with PRISM. We apply this technique to compute the minimal probability of a leader being elected before a deadline, for different deadlines, and study the influence of using a biased coin on this minimal probability.     

Module Checking

In computer system design, we distinguish between closed and open systems. A closed system is a system whose behavior is completely determined by the state of the system. An open system is a system that interacts with its environment and whose behavior depends on this interaction. The ability of temporal logics to describe an ongoing interaction of a reactive program with its environment makes them particularly appropriate for the specification of open systems. Nevertheless, model-checking algorithms used for the verification of closed systems are not appropriate for the verification of open systems. Correct model checking of open systems should check the system with respect to arbitrary environments and should take into account uncertainty regarding the environment. This is not the case with current model-checking algorithms and tools. In this paper we introduce and examine the problem of model checking of open systems (module checking, for short). We show that while module checking and model checking coincide for the linear-time paradigm, module checking is much harder than model checking for the branching-time paradigm. We prove that the problem of module checking is EXPTIME-complete for specifications in CTL and 2EXPTIME-complete for specifications in CTL*. This bad news is also carried over when we consider the program-complexity of module checking. As good news, we show that for the commonly-used fragment of CTL (universal, possibly, and always possibly properties), current model-checking tools do work correctly, or can be easily adjusted to work correctly, with respect to both closed and open systems.     

时间自动机与网络协议验证

随着网络协议复杂性的增大，其自身的潜在错误变得更加重要。使用形式化的方法来描述和验证网络协议可以发现其中的潜在错误。时间自动机是形式化方法的一种，可以很好地应用于网络协议验证中。目前基于时间自动机已经开发出了多种自动验证工具。文章介绍了网络协议验证的几种方法，并以KRONOS验证FDDI协议为例说明了用时间自动机验证协议的方法。     

Solving scheduling problems by untimed model checking

In this article, we show how scheduling problems can be modelled in untimed process algebra, by using special tick actions. A minimal-cost trace leading to a particular action, is one that minimises the number of tick steps. As a result, we can use any (timed or untimed) model checking tool to find shortest schedules. Instantiating this scheme to μCRL, we profit from a richer specification language than timed model checkers usually offer. Also, we can profit from efficient distributed state space generators. We propose a variant of breadth-first search that visits all states between consecutive tick steps, before moving to the next time slice. We experimented with a sequential and a distributed implementation of this algorithm. In addition, we experimented with beam search, which visits only parts of the search space, to find near-optimal solutions. Our approach is applied to find optimal schedules for test batches of a realistic clinical chemical analyser, which performs several kinds of tests on patient samples.     

Towards action refinement for true concurrent real time

Action refinement is an essential operation in the design of concurrent systems, real-time or not. In this paper we develop a theory of action refinement in a real-time non-interleaving causality based setting, a timed extension of bundle event structures that allows for urgent interactions to model timeout. The syntactic action refinement operation is presented in a timed process algebra as incorporated in the internationally standardised specification language LOTOS. We show that the behaviour of the refined system can be inferred compositionally from the behaviour of the original system and from the behaviour of the processes substituted for actions with explicitly represented start points, that the timed versions of a linear-time equivalence, termed pomset trace equivalence, and a branching-time equivalence, termed history preserving bisimulation equivalence, are both congruences under the refinement, and that the syntactic and semantic action refinements developed coincide under these equivalence relations with respect to a metric denotational semantics. Therefore, our refinement operations behave well. They meet the commonly expected properties.Received: 9 January 2003     

Dealing with practical limitations of distributed timed model checking for timed automata

Two base algorithms are known for reachability verification over timed automata. They are called forward and backwards, and traverse the automata edges using either successors or predecessors. Both usually work with a data structure called Difference Bound Matrices (DBMs). Although forward is better suited for on-the-fly construction of the model, the one known as backwards provides the basis for the verification of arbitrary formulae of the TCTL logic, and more importantly, for controller synthesis. Zeus is a distributed model checker for timed automata that uses the backwards algorithm. It works assigning each automata location to only one processor. This design choice seems the only reasonable way to deal with some complex operations involving many DBMs in order to avoid huge overheads due to distribution. This article explores the limitations of Zeus-like approaches for the distribution of timed model checkers.Our findings justify why close-to-linear speedups are so difficult –and sometimes impossible– to achieve in the general case. Nevertheless, we present mechanisms based on the way model checking is usually applied. Among others, these include model-topology-aware partitioning and on-the-fly workload redistribution. Combined, they have a positive impact on the speedups obtained.

Constraint-Based Verification of Parameterized Cache Coherence Protocols

We propose a new method for the parameterized verification of formal specifications of cache coherence protocols. The goal of parameterized verification is to establish system properties for an arbitrary number of caches. In order to achieve this purpose we define abstractions that allow us to reduce the original parameterized verification problem to a control state reachability problem for a system with integer data variables. Specifically, the methodology we propose consists of the following steps. We first define an abstraction in which we only keep track of the number of caches in a given state during the execution of a protocol. Then, we use linear arithmetic constraints to symbolically represent infinite sets of global states of the resulting abstract protocol. For reasons of efficiency, we relax the constraint operations by interpreting constraints over real numbers. Finally, we check parameterized safety properties of abstract protocols using symbolic backward reachability, a strategy that allows us to obtain sufficient conditions for termination for an interesting class of protocols. The latter problem can be solved by using the infinite-state model checker HyTech: Henzinger, Ho, and Wong-Toi, A model checker for hybrid systems, Proc. of the 9th International Conference on Computer Aided Verification (CAV'97), Lecture Notes in Computer Science, Springer, Haifa, Israel, 1997, Vol. 1254, pp. 460–463. HyTech handles linear arithmetic constraints using the polyhedra library of Halbwachs and Proy, Verification of real-time systems using linear relation analysis, Formal Methods in System Design, Vol. 11, No. 2, pp. 157–185, 1997. By using this methodology, we have automatically validated parameterized versions of widely implemented write-invalidate and write-update cache coherence protocols like Synapse, MESI, MOESI, Berkeley, Illinois, Firefly and Dragon (Handy, The Cache Memory Book, Academic Press, 1993). With this application, we have shown that symbolic model checking tools like HyTech, originally designed for the verification of hybrid systems, can be applied successfully to new classes of infinite-state systems of practical interest.     

一种基于时间自动机的域构造方法

模型检验是一种重要的形式化自动验证技术,通过状态空间搜索来保证软硬件设计的正确性。由于TCTL不是针对时间自动机,而是针对有限状态变迁系统的,从而无法使用TCTL直接对时间自动机进行模型检验。给出了一种从时间自动机到有限状态变迁系统的方法,并在不改变时间自动机的语义上,使时间自动机等价后的域状态数尽可能少,在一定程度上有效地解决了状态空间爆炸问题。     

Issues in distributed timed model checking

In this work we present Zeus, a distributed timed model checker that evolves from the TCTL model checker Kronos [13] and that currently can handle backwards computation of reachability properties [2] over timed automata [3].Zeus was developed following a software architecture-centric approach. Its conceptual architecture was conceived to be sufficiently modular to house several features such as a priori graph partitioning, synchronous and asynchronous computation, communication piggybacking, delayed messaging, and dead-time utilization.Surprisingly enough, early experiments pinpointed the difficulties of getting speedups using asynchronous versions and showed interesting results on the synchronous counterpart, although being intuitively less attractive.     

Deadlock-Freeness Analysis of Continuous Mono-T-Semiflow Petri Nets

Most verification techniques for highly populated discrete systems suffer from the state explosion problem. The “fluidification” of discrete systems is a classical relaxation technique that aims to avoid the state explosion problem. Continuous Petri nets are the result of fluidifying traditional discrete Petri nets. In continuous Petri nets the firing of a transition is not constrained to the naturals but to the non-negative reals. Unfortunately, some important properties, as liveness, may not be preserved when the discrete net model is fluidified. Therefore, a thorough study of the properties of continuous Petri nets is required. This paper focuses on the study of deadlock-freeness in the framework of mono-T-semiflow continuous Petri nets, i.e., conservative nets with a single repetitive sequence (T-semiflow). The study is developed both on untimed and timed systems. Topological necessary conditions are extracted for this property. Moreover, a bridge relating deadlock-freeness conditions for untimed and timed systems is established.     

Real-Time Verification Techniques for Untimed Systems

We show that verification techniques for timed automata based on the Alur and Dill region-graph construction can be applied to much more general kinds of systems, including asynchronous untimed systems over unbounded integer variables. We follow this approach in proving that the model-checking problem for the n-process Bakery algorithm is decidable, for any fixed n. We believe this is the first decidability proof for this problem to appear in the literature.