The information listed on this page refers to the state of the tool in '99. For more recent information, please use the following link:

http://www-verimag.imag.fr/TEMPORISE/kronos/

---

KRONOS - VERIMAG

Name: KRONOS

Main Functionalities

Formal verification of real-time systems.

Derived Functionalities

Model-checking:

• Performing symbolic reachability analysis
• Verifying properties specified in timed temporal logic
• Checking Timed Büchi-automata emptiness
• Computing Time-abstracting behavioral equivalences

Synthesis:

• Computing controllers for ensuring safety properties

Description

KRONOS is a software tool built with the aim of assisting designers of real-time systems to verify whether their designs meet the specified requirements.

One major objective of KRONOS is to provide a verification engine to be integrated into design environments for real-time systems in a wide range of application areas, e.g.:

• real-time communication protocols
• timed asynchronous circuits
• hybrid systems

Availability

KRONOS is freely distributed to academic institutions for non-profit use.
It can be downloaded at the following URL:

http://www-verimag.imag.fr/TEMPORISE/kronos

Contact person: S. Yovine (Sergio.Yovine@imag.fr)

Format of the distribution

• Binaries
• Linkable libraries

Supported platforms:

• Linux, Solaris 2.x