Issue No. 09 - September (1992 vol. 18)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.159837
<p>A method for the implementation and analysis of real-time systems, based on the compilation of specification extended automata is proposed. The method is illustrated for a simple specification language that can be viewed as the extension of a language for the description of systems of communicating processes, by adding timeout and watchdog constructs. The main result is that such a language can be compiled into timed automata, which are extended automata with timers. Timers are special state variables that can be set to zero by transitions, and whose values measure the time elapsed since their last reset. Timed automata do not make any assumption about the nature of time and adoptan event-driven execution mode. Their complexity does not depend on the values of the parameters of timeouts and watchdogs used in specifications. These features allow the application on timed automata of efficient code generation and analysis techniques. In particular, it is shown how symbolic model-checking of real-time properties can be directly applied to this model.</p>
real-time specifications; real-time systems; extended automata; simple specification language; communicating processes; timeout; watchdog constructs; timed automata; state variables; event-driven execution mode; complexity; efficient code generation; symbolic model-checking; real-time properties; automata theory; communicating sequential processes; formal specification; program compilers; real-time systems; specification languages
J. Sifakis, X. Nicollin and S. Yovine, "Compiling Real-Time Specifications into Extended Automata," in IEEE Transactions on Software Engineering, vol. 18, no. , pp. 794-804, 1992.