5 Compositional Verification of Timed Systems Saddek Bensalem∗ Abstract In this paper we address the state space explosion problem inherent to model-checking timed systems with a large number of components. The main challenge is to obtain pertinent global timing constraints from the timings in the components alone. To this end, we make use of auxiliary clocks to automat- ically generate new invariants which capture the constraints induced by the synchronisations between components. The method has been implemented as an extension of the D-Finder tool and successfully experimented on several benchmarks. We addressed the problem of state-explosion inherent to model-checking of timed systems built from large number of components. Our solution consists in adapting the compositional verification approach of [BBSN08] to timed systems. The main challenge was to be able to capture the relations between the local timing of the components induced by their interactions. Without them the proposed compositional analysis proved to be too weak for verifying even simple systems. The proposed relations take the shape of equalities between the clocks of components used for expressing their timing constraints. We proved the soundness of the proposed approach, and successfully applied it to academic examples and non trivial case studies. Compositional methods in verification have been developed to cope with state explosion. Generally based on divide-and-conquer principles, compositional methods attempt to break monolithic verification problems into smaller sub-problems by exploiting either the structure of the system or of the property to verify, or both. Compositional reasoning can be used in different flavors, e.g. deductive verification, assume-guarantee reasoning [MC81, Jon83, Pnu84], contract-based verification [DLL+ 12, LLH+ 12], compositional generation, etc. Nonetheless, compositional verification has not been very successfully applied to timed systems. The most used tools for the verification of such systems are based on symbolic state space exploration, using efficient data structures and exploration techniques. Few attempts have been made however for exploiting compositionality principles but they remain marginal in the research literature. Nowadays, it is generally admitted that the difficulty for using compositional reasoning is inherently due to the synchronous model of time. Time progress hides continuous synchronization of all the components of the system. Getting rid of such synchronization is necessary for analyzing independently different parts of the system (or of the property) but also extremely problematic when attempting to re-compose the partial verification results. We proposed a different approach for exploiting compositionality for analysis of timed systems. We developed a novel compositional method for the generation of invariants for timed systems. In contrast to exact reachability analysis, invariants are symbolic approximations of the set of reachable states of the system. We show that quite precise invariants can be computed compositionally, from the separate analysis of the components in the system and from their composition glue. This method is sound for verification of safety properties, that is, if a given property can be deduced from the invariants computed for the system, then the system is guaranteed to satisfy that property. However, the method is not complete, that is, it may be not able to prove certain properties even if they are satisfied by the system. Our Compositional Verification Method. The compositional method we propose here is based on the verification rule (VR) from [BBSN08]. Assume that a system consists of n components Bi interacting by means of an interaction set γ, and that the system property of interest is Φ. If components Bi , respectively interactions γ, can be locally characterized by means of invariants CI (Bi ), respectively II (γ), and if Φ can ∗ This is joint work with L. Aştefănoaei, S. Ben Rayana, M. Bozga, J. Combaz. 1 6 be proved to be a logical consequence of the conjunction of the local invariants, then Φ is a global invariant. This is what the rule below synthesizes. ^ ` CI (Bi ) ∧ II (γ) → Φ i (VR) kγ Bi |= Φ In the rule (VR), the symbol ` is used to underline that the logical implication can be effectively proved (for instance with an SMT solver) and the notation B |= Φ is to be read as “Φ holds in every reachable state of B”. The key idea behind the compositional generation method is to use additional history clocks in order to track the timing of interactions between different components. History clocks allow to decouple the analysis for components and for their composition. On component level, history clocks are used to capture and expose the local timing constraints relevant to their interactions. At composition level, extra constraints on history clocks are enforced due to simultaneity of interactions and to the synchrony of time progress. Timed Systems. In our framework, the components are timed automata [AD94] and systems are com- positions of timed automata with respect to n-ary interactions. Timed automata represent the behavior of components. They have control locations and transitions between these locations. Transitions may have timing constraints, which are defined on clocks. Clocks can be reset and/or tested along with transition ex- ecution. Formally, a timed automaton is tuple (L, l0 , A, T, X, tpc) where L is a finite set of control locations, l0 is an initial control location, A a finite set of actions, X is a finite set of clocks, T ⊆ L × (A × C × 2X ) × L is finite set of transitions labeled with actions, guards, and a subset of clocks to be reset, and tpc : L → C assigns a time progress condition1 to each location. C is the set of timing constraints which are predicates on the clocks X defined by the following grammar: C ::= true | false | x#ct | x − y#ct | C ∧ C with x, y ∈ X, # ∈ {<, ≤, =, ≥, >} and ct ∈ Z. Time progress conditions are restricted to conjunctions of constraints as x ≤ ct. For simplicity, we assume that at each location l the guards of the outgoing transitions imply the time progress condition tpc(l) of l. A timed automaton is a syntactic structure whose semantics is based on continuous and synchronous time progress. That is, a state is given by a control location paired with real-valued assignments of the clocks. From a given state, a timed automaton can let time progresses when permitted by the time progress condition of the corresponding location, or execute a (discrete) transition if its guard evaluates to true. The effect of time progress of δ > 0 is to increase synchronously all the clocks by the the real value δ. Executions of transitions are instantaneous, that is, they keep values of clocks unchanged except the ones that are reset (i.e. assigned to 0). Because of their continuous semantics, timed automata have in general infinite state spaces. However, they admit finite symbolic representations of their state spaces called zone graph [ACD+ 92, Alu99, HNSY94, YPD94], in which equivalent assignments of clocks are grouped in a single (symbolic) state call zone having the shape of timing constraints defined previously. That is, the reachable states of a timed automata corresponds to a finite number of configurations (lj , ζj ), 1 ≤ j ≤ m, where for all j, lj is a control location and ζj is a timing constraint. Examples of timed automata are provided by Figure 1. For instance, components W orkeri , i ∈ {1, 2}, are implemented by similar timed automata, consisting of two control locations l1i and l2i and two transitions: a transition from l1i to l2i labelled by action bi and having timing constraint y ≥ 8, and a transition from l2i to l1i having action di and resetting clock y. By convention non displayed guards of transitions and time progress conditions of locations are true. In our framework, components interact by means of strong synchronization between their actions. The synchronizations are specified in the so called interactions as sets of actions. An interaction can involve at 1 To avoid confusion with invariant properties, we prefer to adopt the terminology of “time progress condition” instead of “location invariants”. 2 7 a lc0 b2 x≥8 b1 l12 x := 0 l11 d2 , b2 , x≤4 lc1 d1 , b1 , y2 := 0 y2 ≥ 8 y1 := 0 y1 ≥ 8 c a, x = 4 l22 x := 0 x:=0 l21 d2 d1 Worker 2 lc2 Worker 1 c Controller Figure 1: A composition of three timed automata. most one action of each component. Given n components (i.e. timed automata) Bi = (Li , l0i , Ai , T i , X i , tpci ), 1 ≤ i ≤ n, and a set of interactions γ, we denote by γ(B1 , . . . , Bn ) the composition of components Bi with respect to interactions γ. States of the composition γ(B1 , . . . , Bn ) are combinations of the states of the components Bi . In γ(B1 , . . . , Bn ), a component Bi can execute an action ai only as part of an interaction α ∈ γ, ai ∈ α, that is, along with the execution of all the actions participating to α, which corresponds to the usual notion of multi-party interaction. Notice that for a component Bi of a composition γ(B1 , . . . , Bn ), the application of interactions γ can only restrict its reachable states. That is, the reachable states of Bi when executed in the composition γ(B1 , . . . , Bn ) are included in the reachable states of Bi executed alone (i.e. as a single timed automata). This property is essential for building our compositional verification method, presented below. Components and Interaction Invariants. To give a logical characterization of a system S = γ(B1 , . . . , Bn ) we use invariants. An invariant Φ is a state property which holds in every reachable state of S, in symbols, S |= Φ. Component invariants CI (Bi ) characterize the reachable states of components Bi when considered alone. Such invariants can easily be computed from the zones of the corresponding timed automata. More precisely, given the reachable (symbolic) states (lj , ζj ), 1 ≤ j ≤ m, of component Bi , the invariant for Bi is defined by: _ lj ∧ ζ j , 1≤j≤m where we abuse of notation and use lj for the predicate that holds whenever Bi is at location lj . Notice that zones ζj are timing constraints, that is, predicates on clocks. Notice also that invariants CI (Bi ) still hold for the composed system S = γ(B1 , . . . , Bn ), but are only over approximations of the states reached by each component Bi in S. For example, the component invariants for Controller , Worker 1 and Worker 2 of Figure 1 are as follows: CI (Controller ) = (lc0 ∧ x ≥ 0) ∨ (lc1 ∧ x ≤ 4) ∨ (lc2 ∧ x ≥ 0) CI (Worker i ) = (l1i ∧ yi ≥ 0) ∨ (l2i ∧ yi ≥ 8). Interaction invariants II (γ) are induced by the synchronizations and have the form of global conditions involving control locations of components. In previous work, we have considered boolean conditions [BBSN08] as well as linear constraints [SBL12] for II (γ). For instance, such invariants exclude configurations such that lc1 ∧ l2i , that is, they establish ¬ lc1 ∧ (l21 ∨ l21 ) . Interaction invariants are not the main purpose of this work, interested readers should refer to [BBSN08] and [SBL12] for detailed presentations. 3 8 A safety property of interest for example of Figure 1 is absence of deadlocks. A necessary condition for deadlock freedom is that a can synchronize with b1 or b2 when the controller is at lc1 and the workers are at l1i , that is, Φ = lc1 ∧ l11 ∧ l12 =⇒ y1 − x ≥ 4 ∨ y2 − x ≥ 4. Even if Φ holds in S, it cannot be proved by applying (VR) using only component invariants CI (Bi ) and interaction invariant II (γ). A counter example is given by lc1 ∧l11 ∧l12 and x = y1 = y2 = 0, which satisfies the invariant CI (Controller )∧CI (Worker 1 )∧CI (Worker 2 )∧ II (γ)2 but violate property Φ, that is, CI (Controller ) ∧ CI (Worker 1 ) ∧ CI (Worker 2 ) ∧ II (γ) =⇒ 6 Φ. One problem is that the proposed invariants cannot relate values of clocks of different components according to their synchronizations (e.g. synchronous reset of clocks). Adding History Clocks. To strengthen computed invariants, we proposed to equip each component Bi (and later, interactions) with history clocks: one clock hai per action of ai of Bi . A history clock hai is reset on all transitions executing ai . Notice that since there is no timing constraint involving history clocks, the behavior of the components remain unchanged after the addition of the history clocks, which shown in [ARB+ 13]. They are only introduced for establishing properties. Each time an interaction α ∈ γ is executed, all the history clocks corresponding to the actions participating in α are reset synchronously, and then become identical at the next state (until another interaction is executed). Moreover, history clocks of actions of the last executed interaction α are necessarily lower than the ones of actions not participating in α, since they are the last being reset. This is captured by the following invariant: _ ^   E(γ) = hai = haj ≤ hak ∧ E(γ α) , α∈γ ai ,aj ∈α ak ∈α / where γ α = {β \ α | β ∈ γ ∧ β 6⊆ α}. It can be shown that E(γ) is an invariant of the system [ARB+ 13]. For example of Figure 1, invariant E(γ) is given by: E(γ) = (ha = hb1 ≤ hb2 ∨ ha = hb2 ≤ hb1 ) ∧ (hc = hd1 ≤ hd2 ∨ hc = hd2 ≤ hd1 ). Component invariants for example of Figure 1 including the history clocks are as follows: CI (Controller h ) = lc0 ∨ (lc1 ∧ x ≤ 4 ∧ (ha = hc ≥ 8 + x ∨ x = hc ≤ ha )) ∨ (lc2 ∧ x = ha ∧ (hc ≥ ha + 12 ∨ hc = ha + 4)) CI (Worker hi ) = (y = hdi ∧ l1i ∧ hdi ≤ hbi ) ∨ (l2i ∧ hdi ≥ 8 + hbi ). Such invariants proved to be sufficient for stating deadlock-freedom for a similar example involving only one worker, but are too weak for establishing deadlock-freedom with two workers. When interactions are conflicting on shared action ai , the proposed invariants for history clock hai always consider that any of these interactions can execute. For instance, in example of Figure 1 our invariants cannot capture the fact that if action a of Controller synchronizes with b1 of Worker 1 , then the following execution of action c of Controller can only synchronize with d1 of Worker 1 (it cannot synchronize with d2 of Worker 2 ). Handling Conflicting Interactions. We developed a general way for computing stronger invariants relating execution of the interactions. The principle is to add again history clocks hα for each the interaction α of γ, and to reset hα each time α is executed by the means of an additional component and adequate synchronizations. A full description of this approach can be found in [ARB+ 13]. For an action ai of component Bi , we define the separation constraint S(γ, ai ) as: ^ S(γ, ai ) = | hα − hβ |≥ δai , α,β∈γ | ai ∈α,β α6=β 2 Notice that interaction invariants cannot exclude lc ∧ l1 ∧ l2 since it is a reachable configuration. 1 1 1 4 9 where δai is a lower bound of the time elapsed between two consecutive executions of ai in Bi , which can be statically computed from the timed automata of Bi . It can be shown [ARB+ 13] that separation constraints S(γ, ai ) are invariants of the system, that is, the following is an invariant of the system: ^ ^ S(γ) = S(γ, ai ). 1≤i≤n ai ∈Ai Invariant E(γ) can be rewritten using additional history clocks as follows: ^ ^ E(γ) = hai = minα3ai hα . 1≤i≤n ai ∈Ai This corresponds to the intuition that the history clock of an action ai equals the history clock of the last executed interaction α involving ai , which is the one having hα minimal. Experimental Results. We have developed a prototype in Scala implementing the approach. It takes as input components Bi , interactions γ, and a global safety property Φ, and checks whether the system satisfy Φ. To this end, it first computes the invariants proposed above, using PPL3 . Then it generates Z34 Python code to check the satisfiability of the following formula: ^ CI (Bi ) ∧ II (γ) ∧ E(γ) ∧ S(γ) ∧ ¬Φ. (1) 1≤i≤n Notice that when γ has no conflicting interactions we can simply use the initial form for E(γ) and discard S(γ). If (1) is not satisfiable then the system is guaranteed to satisfy Φ (i.e. our approach is sound). Otherwise, Z3 returns an assignment of the variables satisfying (1) and corresponding to a global state of the system that violates property Φ. Since we use over-approximations (i.e. invariants) instead of the exact behavior of the system, this state may be not reachable and Φ may actually hold in the system. We experimented the approach on several classical examples, namely the Train-Gate-Controller (TGC ), the Fischer mutual exclusion protocol, and the Temperature-Control-System (TCS ). We compared our pro- totype implementation with Uppaal5 . Uppaal is a widely used model-checker for timed systems implement- ing symbolic reachability of parallel composition of timed automata using zones. We measured execution times for verifying properties of interest for these examples, i.e. mutual exclusion for TGC and Fischer and deadlock-freedom for TCS (see Table 1). Experimental results shown that Uppaal is subject to state- explosion when increasing the number of components, which happened with TCS for 16 components or more, and with Fischer for 14 components or more. In contrast, our prototype managed to verify TCS even for 124 components in less than 20 seconds. We believe that such compositional approach is very interesting for systems composed of large number of identical components (e.g. swarms of robots) since in this case we reuse already computed invariants following incremental approaches of [BGL+ 11]. Conclusion. We have presented a compositional verification method for systems subject to timing con- straints. It relies on invariants computed separately from system components and their interactions. This method is sound for verification of safety properties, that is, it can be used to prove that the system cannot reach an undesirable configuration. We believe that it is suited to check correctness of coordinations within distributed systems, usually implemented by communication protocols relying on time. Its applicability has already been considered in an European project for an ensemble of robots and devices coordinating in real-time to build consistent knowledge and to achieve safe behavior. 3 bugseng.com/products/ppl 4 research.microsoft.com/en-us/um/redmond/projects/z3 5 www.uppaal.org 5 10 Model & Size Time/Space Property Our prototype Uppaal 1 0m0.156s/2.6kB+140B 0ms/8 states Train Gate Controller & 2 0m0.176s/3.2kB+350B 0ms/13 states mutual exclusion 64 0m4.82s/530kB+170kB 0m0.210s/323 states 124 0m17.718s/700kB+640kB 0m1.52s/623 states 2 0m0.144/3kB 0m0.008s/14 states Fischer & 4 0m0.22s/6.5kB 0m0.012s/156 states mutual exclusion 6 0m0.36s/12.5kB 0m0.03s/1714 states 14 0m2.840s/112kB no result in 4 hours 1 0m0.172s/840B+60B 0m0.01s/4 states Temperature Controller & 8 0m0.5s/23kB+2.4kB 11m0.348s/57922 states absence of deadlock 16 0m2.132s/127kB+9kB no result in 6 hours 124 0m19.22s/460kB+510kB no result in 6 hours Table 1: Experimental results for model-checking tool Uppaal and our prototype tool. References [ACD+ 92] Rajeev Alur, Costas Courcoubetis, David L. Dill, Nicolas Halbwachs, and Howard Wong-Toi. An implementation of three algorithms for timing verification based on automata emptiness. In RTSS, pages 157–166, 1992. [AD94] Rajeev Alur and David L. Dill. A theory of timed automata. Theor. Comput. Sci., 126(2):183– 235, 1994. [Alu99] Rajeev Alur. Timed automata. In Proceedings of the 11th International Conference on Computer Aided Verification (CAV), LNCS, pages 8–22. Springer, 1999. [ARB+ 13] Lăcrămioara Aştefănoaei, Souha Ben Rayana, Saddek Bensalem, Marius Bozga, and Jacques Combaz. Compositional invariant generation for timed systems. Technical Report TR-2013-5, Verimag Research Report, 2013. [BBSN08] Saddek Bensalem, Marius Bozga, Joseph Sifakis, and Thanh-Hung Nguyen. Compositional ver- ification for component-based systems and application. In Proceedings of the 6th International Symposium on Automated Technology for Verification and Analysis, ATVA ’08, pages 64–79, Berlin, Heidelberg, 2008. Springer-Verlag. [BGL+ 11] Saddek Bensalem, Andreas Griesmayer, Axel Legay, Thanh-Hung Nguyen, Joseph Sifakis, and Rongjie Yan. D-finder 2: Towards efficient correctness of incremental design. In Mihaela Gheo- rghiu Bobaru, Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi, editors, NASA Formal Methods, volume 6617 of Lecture Notes in Computer Science, pages 453–458. Springer, 2011. [DLL+ 12] Alexandre David, Kim Guldstrand Larsen, Axel Legay, Mikael H. Møller, Ulrik Nyman, Anders P. Ravn, Arne Skou, and Andrzej Wasowski. Compositional verification of real-time systems using Ecdar. STTT, 2012. [HNSY94] Thomas A. Henzinger, Xavier Nicollin, Joseph Sifakis, and Sergio Yovine. Symbolic model check- ing for real-time systems. Inf. Comput., 111(2):193–244, June 1994. [Jon83] Cliff B. Jones. Specification and design of (parallel) programs. pages 321–332, 1983. [LLH+ 12] Shang-Wei Lin, Yang Liu, Pao-Ann Hsiung, Jun Sun, and Jin Song Dong. Automatic generation of provably correct embedded systems. In ICFEM, 2012. 6 11 [MC81] Jayadev Misra and Kanianthra Mani Chandy. Proofs of networks of processes. page 4:417426, 1981. [Pnu84] Amir Pnueli. In transition from global to modular temporal reasoning about programs. page 123144, 1984. [SBL12] Marius Bozga Saddek Bensalem, Benoit Boyer and Axel Legay. Incremental generation of lin- ear invariants for component-based systems. Technical Report TR-2012-15, Verimag Research Report, 2012. [YPD94] Wang Yi, Paul Pettersson, and Mats Daniels. Automatic verification of real-time communicating systems by constraint-solving. In FORTE, pages 243–258, 1994. 7