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.