Abstract:

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.