Database of Research Tools Developed Using CADP

KRONOS-OPEN Tool for Real-Time Verification

Organisation: VERIMAG laboratory (Grenoble, FRANCE)

Functionality: Verification of real-time systems

Tools used: OPEN/CAESAR

Period: 1998-1999

Description: 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.

Conclusions: 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.

Publications: [Tripakis-99] Stavros Tripakis. "Extended Kronos/CADP Tool: Minimization, On-the-Fly Verification and Compositionality". Technical Report T226, VERIMAG, Grenoble, France, April 1999.
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
Contact:
Stavros Tripakis
VERIMAG
2, avenue de Vignate
38610 Gières
FRANCE
E-mail: Stavros.Tripakis@imag.fr



Further remarks: This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software


Last modified: Fri Feb 19 09:13:01 2016.


Back to the CADP research tools page