A timed automaton model for ET-LOTOS verification

Abstract

We present in this paper a method to transform ET-LOTOS expressions in a subclass of timed automaton with timers, where a timer is not restarted before its reset. We show that this subclass is equivalent to timed automata and we show that this model can be used for ET-LOTOS verification. We have implemented this transformation method and interfaced our tool with the KRONOS model-checker. It is then possible to verify temporal properties, expressed in TCTL, on ET-LOTOS specifications. We illustrate our tool with a small robot controller example.