Verifying ET-LOTOS programmes with KRONOS.
Conrado Daws, Alfredo Olivero, Sergio Yovine · Formal Techniques for (Networked and) Distributed Systems · 1994
ET-LOTOS is a timed extension of LOTOS proposed for modeling real-time systems. KRONOS is a tool that checks whether an automaton extended with clocks (called timed automaton) satisfies a real-time requirement expressed as a formula of the logic TCTL. This paper shows that real-time systems described in a reasonable subset of ET-LOTOS can be verified with KRONOS by compiling them into timed automata. We illustrate the practical interest of our approach with a case study: the Tick-Tock protocol.