VERIMAG laboratory (Grenoble, FRANCE)
Verification of real-time systems
KRONOS is a tool suite for the analysis of real-time systems, developed
at VERIMAG since 1992. It allows, among other functionalities, TCTL and
reachability model-checking on timed automata. The "first-generation"
of KRONOS was built from modules acting as interpreters, i.e.,
performing the analysis directly on their input model.
The C code generator module KRONOS-OPEN, based on the compiler approach, represents the "next generation" of KRONOS. Given an input model, KRONOS-OPEN produces C-code that can be in turn compiled to various executables performing the analysis of the specific input model. Another difference from the first-generation tools is that KRONOS-OPEN accepts a richer input language, namely timed automata with bounded discrete variables and shared-variable or message-passing communication.
KRONOS-OPEN takes as input a LOTOS-like expression specifying the system components and their channel connection. Each timed automaton together with its variables is contained in a separate file. KRONOS-OPEN creates a C file implementing the on-the-fly generation of the simulation graph of the input model. The core of the C file consists of the data structures to represent symbolic states (zones) and edges, an the implementation of the "successor" function. This C file is compiled and linked to OPEN/CAESAR and polyhedra DBM libraries, producing a program that performs a certain type of analysis. Besides the OPEN/CAESAR tools already available in CADP (XSIMULATOR, GENERATOR, EXHIBITOR, and EVALUATOR), a new tool called PROFOUNDER, performing reachability analysis, has been developed.
Compared to the interpreter one, the compiler approach implemented
in KRONOS-OPEN has important benefits: guards, assignments and clock
resets are transformed directly to C code, which results in a more
efficient execution than having generic functions for these operations.
In particular, when the above operations are trivial (e.g., true guard,
no assignment) they can be completely skipped.
"Extended Kronos/CADP Tool: Minimization, On-the-Fly Verification and
Compositionality". Technical Report T226, VERIMAG, Grenoble, France,
Available on-line at: http://radon.ics.ele.tue.nl/~vires/reports/year2/wp2/t226/tripakis99.ps
or also from our FTP site in PDF or PostScript
2, avenue de Vignate
|Further remarks:||This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software|