next up previous

Final Report of the COST-247 Action

Kronos: A Tool for Verifying Real-time Systems

Sergio Yovine

Centre Equation
2, avenue de Vignate
F-38610 Gieres
tel : +(33) 4 76 63 48 48
fax : +(33) 4 76 63 48 50


Kronos is a tool that performs symbolic model-checking for real-time systems. It reads a timed graph describing a real-time system and a TCTL formula specifying a requirement, and checks whether the timed graph satisfies the formula. Timed graphs are automata extended with a finite set of real-valued clocks, used to express timing constraints. TCTL is an extension of the temporal logic CTL that allows quantitative temporal reasoning. We first review the main theoretical results and then we show the performances obtained with Kronos in some case studies, in particular the Tick-Tock protocol.

This presentation has been given during the COST-247 WG1 Special Workshop on Extended Process Algebras (Brighton, United Kingdom, July 19--20, 1994).

COST-247 Working Group(s): 1

This Page was prepared by Mark Jorgensen.

Back to the VASY Home page