Tools for the verification of reactive systems

Reactive systems are programs which maintain interactive relations with users and are subject to time dependent requirements. Among those, real-time or hybrid systems form a large subclass where time is handled in an explicit way. A real-time system is usually modeled by a network of automata or graphs, each one having, in addition to a finite number of control locations, special variables which evolve continuously inside locations and may be updated by discrete transitions. In timed automata, there is only one class of such variables, called clocks, which all evolve at precisely the rate of time.

Specific verification tools have been designed to deal with real-time systems, which are noticeably more difficult to analyse than finite state systems. The tools presented below belong to the family known as Model-Checking tools, although some of them actually do not possess the whole power of a model-checker. They are mostly originated in academic work and, except maybe UPPAAL, are not yet friendly or powerful enough to have reached full industrial extent, but they certainly have promising features, worth looking at. This is undoubtly the reason why they can be freely accessed. Apologies for other tools, that I don't know of and therefore did not test, but may exist somewhere. I would be very happy to hear from them.

CMC, developed by F. Laroussinie at LSV, is a Compositional Model-Checker for Lnu, devoted to the analysis of timed automata. Communication between different components of a system is based on the most general technique of synchronization tables.

HyTech can be used for reachability analysis of linear hybrid automata with parameters. Transitions from different automata synchronize on identical labels. See for instance Verification of ABR protocol and LSV Research Report LSV-98-12: Automatic verification of a parametric real-time program: the ABR conformance protocol for a LSV case study with HyTech.

KRONOS is a TCTL (Timed Computational Tree Logic) Model-Checker, which applies to timed graphs. The synchronization function, while not as general as in CMC, is an extension of both UPPAAL and HyTech modes.

UPPAAL proposes reachability analysis and graphic simulation for networks of timed automata, equipped with integer variables. The communication mode between automata is restricted to binary synchronization.