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 automatically 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.
be proved to be a logical consequence of the conjunction of the local invariants, then This is what the rule below synthesizes.
is a global invariant. ` ^CI (Bi) ^ II ( ) ! i k Bi j= (VR) In the rule (VR), the symbol ` is used to underline that the logical implication can be e ectively proved (for instance with an SMT solver) and the notation B j= 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 di erent 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 compositions 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 de ned on clocks. Clocks can be reset and/or tested along with transition execution. Formally, a timed automaton is tuple (L; l0; A; T; X; tpc) where L is a nite set of control locations, l0 is an initial control location, A a nite set of actions, X is a nite set of clocks, T L (A C 2X ) L is nite 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 de ned by the following grammar:
C ::= true j false j x#ct j x y#ct j C ^ C with x; y 2 X, # 2 f<; ; =; ; >g and ct 2 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 e ect 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 in nite state spaces. However, they admit nite 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 de ned previously. That is, the reachable states of a timed automata corresponds to a nite number of con gurations (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 2 f1; 2g, 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 speci ed in the so called interactions as sets of actions. An interaction can involve at 1To avoid confusion with invariant properties, we prefer to adopt the terminology of \time progress condition" instead of \location invariants". Worker 2 b2 d2 most one action of each component. Given n components (i.e. timed automata) Bi = (Li; l0i; Ai; T i; Xi; 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 2 , ai 2 , 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 veri cation 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 j= .
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 de ned by: 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 CI (Worker i) = (l1i ^ yi 0) _ (lc1 ^ x 4) _ (lc2 ^ x
0) 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 con gurations 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.
_ 1 j m lj ^ j ;
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 ^l1 ^l12 and x = y1 = y2 = 0, which satis es the invariant CI (Controller )^CI (Worker 1)^CI (Worker 2)^ 1 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 di erent 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 2 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 ( ) = _ 2
^ ai;aj2 ak2= hai = haj hak ^ E ( ) ; where = f n j 2 ^ 6 g. 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 CI (Worker ih) = (y = hdi ^ l1 ^ hdi i
ha + 12 _ hc = ha + 4)) hbi ) _ (l2i ^ hdi 8 + hbi ): Such invariants proved to be su cient 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 con icting 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 Con icting 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 de ne the separation constraint S( ; ai) as:
S( ; ai) = j h h j ai ; 2Notice that interaction invariants cannot exclude lc1 ^ l11 ^ l12 since it is a reachable con guration.
^ ; 2 j ai2 ; 6= 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: Invariant E ( ) can be rewritten using additional history clocks as follows:
S( ) = ^
^ S( ; ai): 1 i n ai2Ai E ( ) = ^
^ 1 i n ai2Ai
hai = min 3ai h : 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 rst computes the invariants proposed above, using PPL3. Then it generates Z34 Python code to check the satis ability of the following formula:
^ 1 i n
CI (Bi) ^ II ( ) ^ E ( ) ^ S( ) ^ : : (1) Notice that when has no con icting interactions we can simply use the initial form for E ( ) and discard S( ). If (1) is not satis able 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 prototype implementation with Uppaal5. Uppaal is a widely used model-checker for timed systems implementing 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 stateexplosion 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 veri cation method for systems subject to timing constraints. It relies on invariants computed separately from system components and their interactions. This method is sound for veri cation of safety properties, that is, it can be used to prove that the system cannot reach an undesirable con guration. 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.
3bugseng.com/products/ppl 4research.microsoft.com/en-us/um/redmond/projects/z3 5www.uppaal.org
absence of deadlock
Size [AD94]
Rajeev Alur and David L. Dill. A theory of timed automata. Theor. Comput. Sci., 126(2):183{ 235, 1994.
Rajeev Alur. Timed automata. In Proceedings of the 11th International Conference on Computer Aided Veri cation (CAV), LNCS, pages 8{22. Springer, 1999. [ARB+13] Lacramioara Astefanoaei, 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 veri cation for component-based systems and application. In Proceedings of the 6th International Symposium on Automated Technology for Veri cation and Analysis, ATVA '08, pages 64{79, Berlin, Heidelberg, 2008. Springer-Verlag. [DLL+12] Alexandre David, Kim Guldstrand Larsen, Axel Legay, Mikael H. M ller, Ulrik Nyman, Anders P.
Ravn, Arne Skou, and Andrzej Wasowski. Compositional veri cation of real-time systems using Ecdar. STTT, 2012. [HNSY94] Thomas A. Henzinger, Xavier Nicollin, Joseph Sifakis, and Sergio Yovine. Symbolic model checking for real-time systems. Inf. Comput., 111(2):193{244, June 1994.