The tool Kronos

Abstract

Both approaches presented in this paper considerably improve Kronos performance and functionalities.

Forward analysis permits handling examples with a large number of clocks, as the example of the FDDI protocol shows: up to 25 clocks, which, to our knowledge, exceeds the clock-space dimension of similar examples treated in the literature. Moreover, this method is capable of providing a counter-example sequence, as a diagnosis in the case a system fails to verify an invariance or bounded response property.

Minimization considerably reduces the number of states and transitions of large systems, as the example of Fischer's protocol illustrates. It also allows for further analysis, using standard techniques for untimed systems, such as comparison and reduction with respect to behavioral equivalences. The combination of timed and untimed minimization allowed us to discover the problem of starvation in the first version of the mutual-exclusion protocol.

We stress the fact that Fischer's protocol has been analyzed many times, using other real-time verification tools. in particular in [2, 13]. None of these two analyses, however, deals with starvation, while the versions of the protocol used are simpler.

Finally, both forward analysis and minimization prove helpful not only for verification but also for revealing intrinsic problems of modelization, thus giving better insight to the system analyzed.

VERIMAG is a joint laboratory of CNRS, INPG, Université Joseph Fourier, and Verilog SA, associated with IMAG.