The tool Kronos

KRONOS is a tool developed with the aim to verify complex real-time systems.

Real-time systems are systems that must perform a task within strict time deadlines. Embedded controllers, circuits and communication protocols are examples of such time-dependent systems. These systems are often part of complex safety-critical applications such as aircraft avionics, which are very difficult to design and analyze, but whose correct behavior must be ensured because failures may have severe consequences. Hence, real-time systems need to be rigorously modeled and specified in order to be able to formally prove their correctness with respect to the desired requirements.

In KRONOS, components of real-time systems are modeled by timed automata and the correctness requirements are expressed in the real-time temporal logic TCTL.

Timed automata are automata extended with a finite set of real-valued clocks, used to express timing constraints. Clocks can be set to zero and their values increase uniformly with time. At any instant the value of a clock is equal to the time elapsed since the last time it was reset. A transition is enabled only if the timing constraint associated with it is satisfied by the current values of the clocks.

TCTL is an extension of the temporal logic CTL that allows quantitative temporal reasoning over dense time.

KRONOS checks whether a timed automaton satisfies a TCTL-formula.

The model-checking algorithm is based upon a symbolic representation of the infinite state space by sets of linear constraints.

KRONOS is freely distributed to academic institutions for non-profit use.

Last Release

Version: 2.4
Release: 3
Date:Mon Oct 18 15:00:25 MET DST 1999
Executables for
Sun Solaris 5.7 (sun5)
User's guide:
Kronos: A verification tool for real-time systems.

Previous Release

Version: 2.4
Release: 2
Date: Tue Jun 22, 1999
Executables for
Sun Solaris 5.7 (sun5)

Some Older Versions

Version: 2.2b.
Date: Sat Feb 6, 1999.
Executables for
Sun Solaris 2.5 (sun5)

Version: 2.1a.
Date:Nov 19, 1996.
Executables for
Sun Solaris 2.5 (sun5)
Sun OS 4.1 (sun4) No longer supported
HP (hp735) No longer supported
DEC 5000 (dec5000) No longer supported
Manual pages

Examples: examples.tar.gz

Related bibliography.

OPTIKRON, the clock optimizer for KRONOS is also available .

Please contact the authors for questions and comments about KRONOS.

Authors (in order of appeareance)

Other contributors: Luis Sierra, Florence Pagani, Roberto Lublinerman, Marius Bogoevici.

Maintained by Sergio Yovine.

Last modified: March 19, 1999.