|Final Report of the COST-247 Action|
Kronos: A Tool for Verifying Real-time Systems
|2, avenue de Vignate|
|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.