The ZC tool

Download the ZC tool: zc03-12-2009.zip

Background

The semantics of timed automata (Alur & Dill, 1994) (Henzinger, Nicollin, Sifakis, & Yovine, 1994) allow anomalous executions where time does not diverge. These executions take the form of Zeno runs, which are infinite executions with finite accumulated delay, or timelocks, which are states where no subsequent execution allows time to pass beyond a given bound. Zeno runs typically occur in cycles in the model that do not enforce minimum delays between consecutive iterations. Timelocks typically occur due to mismatched synchronisation of urgent actions . Zeno runs and timelocks are counterintuitive because they do not correspond to the real behavior of physical processes. However, more importantly, models with Zeno runs or timelocks cannot be reliably verified, as such behaviours may prevent the model-checker from exploring the complete state space.

Some verification tools, such as Kronos (Yovine, 1997), Red (Wang, 2004) and Profounder (Tripakis, Yovine, & Bouajjani, 2005), avoid Zeno runs during exploration of the state space at the expense of complex algorithms. Instead, the model-checker Uppaal (Behrmann, David, & Larsen, 2004) runs more efficient verification algorithms but does not distinguish time-divergent from Zeno runs; thus, it is the user’s responsibility to ensure that the input model is time-divergent (a sanity test). Uppaal’s requirements language is expressive enough to characterise time-divergence via an unbounded liveness property (this requires the addition of a component that resets a fresh clock at every time unit, and a leads-to property that checks that all executions from all reachable states allow the clock to increment one time unit). However, the verification of this time-divergence property usually demands substantial memory and time to complete, and does not scale up (for instance, Uppaal disallows symmetry reduction when verifying leads-to properties). Hence, state explosion may prevent Uppaal from verifying time-divergence, and consequently the user may have less confidence in the verification of the correctness requirements he or she is interested in.

Often, however, the absence of Zeno runs in the model can be guaranteed by the existence of suitable clock constraints and resets in the model’s cycles. Moreover, models that are free from deadlocks and free from Zeno runs are also free from timelocks. For a given cycle, the strong non-Zenoness property (Tripakis, 1999) holds if there is a clock that is both bounded from below (by a positive constant) and reset in the cycle. Cycles that are strongly non-Zeno (SNZ) cannot be iterated infinitely often with finite accumulated delay fast. Hence, timed automata where all cycles are SNZ are free from Zeno runs. In (Bowman & Gomez, 2006), we showed that this test could be made both more efficient and more precise, as not all cycles in a model need to be SNZ to ensure absence of Zeno runs.

If no elementary non-SNZ cycle (in any component of the network) may complete a full traversal without necessarily synchronising with a SNZ elementary cycle (in any other component of the network), then the network is free from Zeno runs.

The ZC tool is an efficient implementation of the above test for Uppaal networks (Gomez & Bowman, 2007), and offers a lightweight alternative to the verification of time-divergence via liveness analysis (the check is syntactic, compositional and conservative).

The ZC tool, in a nutshell

The ZC tool returns the set of all non-SNZ loops (elementary cycles in components of the network) where Zeno runs may possibly occur. If no such loop is found, the network is guaranteed to be free from Zeno runs. The set of unsafe loops are returned in the XML format of Uppaal networks, so they can be display directly in Uppaal’s GUI. The tool attempts to minimise false positives, that is, loops that are reported as unsafe but do not exhibit Zeno runs. The tool’s main features are summarised below.

1. The ZC tool only reports non-SNZ loops that either do not contain synchronising transitions, or may complete iterations by synchronizing with other non-SNZ loops but without requiring synchronisation with SNZ loops (otherwise, synchronisation with SNZ loops would guarantee absence of Zeno runs).

2. The ZC tool checks that groups of synchronising non-SNZ loops do not contain a shared clock that is reset in some loop in the group, and bounded from below in some other loop in the group (in which case, the joint synchronisation of loops in the group would prevent the occurrence of Zeno runs).

3. The ZC tool does not report non-SNZ loops that contain at least one local integer variable (v, say) that is updated at most once in some transition in the loop, where the update is of the form: v++ | ++v | v+=c | v (=|:=) | v+c (where c is a positive Uppaal constant expression). Such updates ensure that the loop in question may only be traversed finitely often with finite accumulated delay (integer variables in Uppaal have bounded domains, and any assignment out of bounds aborts the verification/simulation).

4. For those Uppaal networks where unsafe template loops are reported, ZC may be instructed (option -p) to instantiate parameters and re-run the analysis over the resulting process loops. In some Uppaal networks (e.g., \demo\bridge.xml in Uppaal distributions) some template loops have clocks which are bounded from below by parametric expressions. It may be the case that all possible values of the parameter yield SNZ process loops, but this cannot be determined solely from the structure of the template loop (i.e., when all SNZ witnesses depend on parameters). Similarly, the analysis on template loops may miss safe synchronisation scenarios (e.g., between NSNZ and SNZ process loops) which may only be discovered after parameterized channels have been resolved to their actual values (e.g., \demo\2doors.xml in Uppaal distributions). We have implemented a second stage analysis that does its best to discover safe instances of template loops (those loops reported by the first analysis), dismissing any template loop for which all of its process loops can be deemed safe.

5. The set of unsafe loops, as reported by the ZC tool, may be used to define a conservative abstraction of the original network, whose state space is an overapproximation of the possible executions of unsafe loops in the original network (Gomez & Bowman, 2007). The abstract network will typically exhibit a much reduced state space, where the absence of Zeno runs can be asserted efficiently by checking Uppaal’s time-divergence property. If the time-divergence property fails to hold on the abstract network, the counterexample may not necessarily represent a Zeno run in the original network. However, in this case, one may attempt to refine the abstraction to avoid the spurious counterexample, in a CEGAR fashion (Dierks, Kupferschmid, & Larsen, 2007).

6. In a complementary way, it is also possible to rule out the occurrence of Zeno runs on a given unsafe loop, by checking that only a (user-defined) finite number of traversals may occur with finite accumulated delay (Gomez, 2006). This check reduces to a simple Uppaal reachability query (this will require annotating the loop with fresh integer and clock variables) and may be more efficient than verifying Uppaal’s time-divergence property.

7. The ZC tool can also be used to check for absence of Zeno runs in Timed Automata with Deadlines (Bornot, Sifakis, & Tripakis, 1998) (Bowman, 2001). In this case, the input model must be given in the same (XML) format expected by our TAD2TA tool (Gomez, 2008).

Details on the tool’s inputs, outputs, and general usage can be found in the file readme.txt, included in the distribution. Examples are also provided in the distribution. We have also written some notes on the use of the ZC tool and Uppaal to verify time-divergence.

Credits

- Java (http://www.sun.com/java/) is a trademark of Sun Microsystems, Inc., and refers to Sun's Java programming language.

- Uppaal (http://www.uppaal.com/) by Uppsala University and Aalborg University.

- CUP LALR Parser Generator (http://www2.cs.tum.edu/projects/cup/) by Scott Hudson, Frank Flannery, C. Scott Ananian

- JFlex The Fast Scanner Generator for Java (http://www.jflex.de/) by Gerwin Klein.

- JSAP The Java-based Simple Argument Parser (http://www.martiansoftware.com/jsap/index.html) by Marty Lamb

- The first version of ZC evolved from a prototype tool developed by Li Su (Su, 2003).

References

Alur, R., & Dill, D. (1994). A theory of timed automata. Theoretical Computer Science , 126, 183-235.

Behrmann, G., David, A., & Larsen, K. G. (2004). A tutorial on Uppaal. Formal methods for the design of real-time systems (SFM-RT 2004). LNCS 3185, pp. 200-236. Bertinoro, Italy: Springer.

Bornot, S., Sifakis, J., & Tripakis, S. (1998). Modelling urgency in timed systems. Compositionality: The Significant Difference (COMPOS' 97). LNCS 1536, pp. 103-129. Bad Malente, Germany: Springer.

Bowman, H. (2001). Time and action-lock freedom properties for timed automata. Formal Techniques for Networked and Distributed Systems (FORTE '01) (pp. 119-134). Cheju Island, Korea: Kluwer Academic Publishers.

Bowman, H., & Gomez, R. (2006). How to stop time stopping. Formal Aspects of Computing , 18 (4), 459-493.

Dierks, H., Kupferschmid, S., & Larsen, K. (2007). Automatic Abstraction Refinement for Timed Automata. FORMATS'07 , LNCS 4763, pp. 114-129.

Gomez, R. (2006). Compositional Detection of Zeno behavior in Timed Automata. Technical Report 12-06, University of Kent, Computing Laboratory.

Gomez, R. (2008). Verification of Timed Automata with Deadlines in Uppaal. Technical report 2-08, University of Kent, Computing Laboratory.

Gomez, R., & Bowman, H. (2007). Efficient detection of Zeno runs in Timed Automata. Proceedings of the 5th International Conference, Formal Modelling and Analysis of Timed Systems, FORMATS'07 (pp. 195-210). Springer.

Henzinger, T., Nicollin, X., Sifakis, J., & Yovine, S. (1994). Symbolic Model Checking for Real-time Systems. Information and Computation , 111 (2), 193-244.

Su, L. (2003). Verification of concurrent systems. Computing Laboratory, University of Kent.

Tripakis, S. (1999). Verifying time progress in timed systems. ARTS'99 , LNCS 1601, pp. 299-314.

Tripakis, S., Yovine, S., & Bouajjani, A. (2005). Checking Timed Buchi Automata efficiently. Formal methods in systems design , 23 (6), 267-292.

Wang, F. (2004). Model-checking distributed real-time systems with states, events, and multiple fairness assumptions. AMAST'04 , LNCS 3116, pp. 553-568.

Yovine, S. (1997). Kronos: A verification tool for real-time systems. Software Tools for Technoloy Transfer , 1 (1/2), 123-133.