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 the CADP Web site in PDF or PostScript
Contact:	Stavros Tripakis VERIMAG 2, avenue de Vignate 38610 Gières FRANCE E-mail: [email protected]
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page