Compiling real-time specifications into extended automata
- 1 September 1992
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Software Engineering
- Vol. 18 (9), 794-804
- https://doi.org/10.1109/32.159837
Abstract
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 adopt an 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.<>Keywords
This publication has 10 references indexed in Scilit:
- Symbolic model checking for real-time systemsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Symbolic model checking: 10/sup 20/ states and beyondPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Model-checking for real-time systemsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- The Algebra of Timed Processes, ATP: Theory and ApplicationInformation and Computation, 1994
- A really temporal logicPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1989
- Applications of temporal logic to the specification of real time systemsLecture Notes in Computer Science, 1988
- A Graph-Theoretic Approach for Timing Analysis and its ImplementationIEEE Transactions on Computers, 1987
- Statecharts: a visual formalism for complex systemsScience of Computer Programming, 1987
- Automatic verification of finite-state concurrent systems using temporal logic specificationsACM Transactions on Programming Languages and Systems, 1986
- The ESTEREL synchronous programming language and its mathematical semanticsLecture Notes in Computer Science, 1985