This Article 
 Bibliographic References 
 Add to: 
Compiling Real-Time Specifications into Extended Automata
September 1992 (vol. 18 no. 9)
pp. 794-804

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.

[1] R. Alur, C. Courcoubetis, and D. Dill, "Model-checking for real-time systems," inProc. 5th Annual IEEE Symp. Logic in Computer Science, pp. 414-425, 1990.
[2] R. Alur and T. Henzinger, "A really temporal logic," inProc. 30th Symp. Foundations of Computer Science, pp. 164-169, IEEE Computer Society Press, 1989.
[3] R. Alur and T. Henzinger, "Logics and models of real-time: A survey," inProc. REX Workshop Real-Time: Theory in Practice, Lecture Notes in Computer Science 600, Springer-Verlag, The Netherlands, June 1991.
[4] R. Alur, "Techniques for automatic verification of real-time systems," Ph.D. dissertation, Department of Computer Science, Stanford Univ., Aug. 1991.
[5] A. V. Aho, R. Sethi, and J. D. Ullman,Compilers: Principles, Techniques, and Tools. Reading, MA: Addison-Wesley, 1986.
[6] G. Berry and L. Cosserat, "The Esterel synchronous programming language and its mathematical semantics," inProc. CMU Seminar on Concurrency, Lecture Notes in Computer Science 197, Springer-Verlag, 1985.
[7] J. B. Burchet al., "Symbolic model checking: 1020states and beyond," inProc. 5th Symp. Logics in Computer Science, pp. 428-439, IEEE Computer Society Press, 1990.
[8] E. M. Clarke, E. A. Emerson, and A. P. Sistla, "Automatic verification of finite-state concurrent systems using temporal logic,"ACM Trans. Program. Lang. Syst., vol. 8, no. 2, pp. 244-263, Apr. 1986.
[9] P. Caspi, D. Pilaud, N. Halbwachs, and J. Plaice, LUSTRE: A declarative language for programming synchronous systems," in14th ACM Symposium on Principles of Programming Languages, Jan. 1987.
[10] E. A. Emerson and E. Clarke, "Design and synthesis of synchronization skeletons using branching-time temporal logic," inProc. Workshop Logic of Programs, Lecture Notes in Computer Science 131, Springer-Verlag, 1981.
[11] H. Garavel, "Compilation et verification de programmes LOTOS," thesis, UniversitéJoseph Fourier, Grenoble, 1989.
[12] P. Le Guernic, A. Benveniste, P. Bournal, and T. Gauthier, "Signal: a data flow oriented language for signal processing,"Tech. Rep. 246, IRISA, Rennes, France, 1985.
[13] H. A. Hanson, "Time and probability in formal design of distributed systems," Ph.D. dissertation, Uppsala Univ., Sweden, Sept. 1991.
[14] D. Harel, "Statecharts: A visual formalism for complex systems,"Sci. Comput. Program., vol. 8, pp. 231-274, 1987.
[15] T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, "Symbolic model-checking for real-time systems," inProc. 7th Symp. Logics in Computer Science, IEEE Computer Society Press, 1992.
[16] IEEE. ANSI/IEEE 802.3, ISO/DIS 8802/3. IEEE Computer Society Press, 1985.
[17] D. M. Jackson, "The specification of aircraft engine control software using Timed CSP," Master's thesis, Univ. Oxford, 1989.
[18] F. Jahanian and A. K. Mok, "A graph-theoretic approach for timing analysis and its implementation,"IEEE Trans. Comput., vol. 36, pp. 961-975, Aug. 1987.
[19] R. Koymans, "Specifying message passing and time critical systems with temporal logic," Ph.D. dissertation, Eindhoven Univ. Technology, May 1989.
[20] X. Nicollin, "ATP : une algèbre pour la spécification et l'analyse des systèmes temps réel, Thesis, INPG, Grenoble, May 1992.
[21] X. Nicollin, J.-L. Richier, J. Sifakis, and J. Voiron, "ATP: An algebra for timed processes," inProc. IFIP TC 2 Working Conference on Programming Concepts and Methods, Israel, Apr. 1990.
[22] X. Nicollin and J. Sifakis, "The algebra of timed processes ATP: Theory and application,"Tech. Rep. RT-C26, LG1-IMAG, France, Dec. 1990, To appear inInformation and Computation.
[23] X. Nicollin and J. Sifakis, "An overview and synthesis on timed process algebras," inProc. 3rd Workshop Computer-Aided Verification, Denmark, July 1991.
[24] X. Nicollin, J. Sifakis, and S. Yovine, "From ATP to timed graphs and hybrid systems," inProc. REX Workshop "Real-Time: Theory in Practice,"Lecture Notes in Computer Science 600, Springer-Verlag, The Netherlands, June 1991.
[25] J. Ostroff,Temporal Logic of Real-Time Systems. Research Studies Press, 1990.
[26] J. Parrow, "Verifying a CSMA/CD-protocol with CCS"Tech. Rep., Laboratory of Foundations of Computer Science, University of Edinburgh, Dec. 1986.
[27] A. Pnueli and E. Harel, "Applications of temporal logic to the specification of real-time systems," inProc. Formal Techniques in Real-Time and Fault-Tolerant Systems (LNCS 331), pp. 84-98, 1988.
[28] J. P. Queille and J. Sifakis, "Specification and verification of concurrent systems in Cesar," inInt. Symp. Programming, LNCS 137. Springer Verlag, Apr. 1982.
[29] A. S. Tanenbaum,Computer Networks, Englewood Cliffs, NJ: Prentice-Hall, 1981.
[30] S. Yovine, "Graph of timers: An approach to translate ATP into timed graphs,"Tech. Rep., LGI-IMAG, France, Sept. 1991.

Index Terms:
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
X. Nicollin, J. Sifakis, S. Yovine, "Compiling Real-Time Specifications into Extended Automata," IEEE Transactions on Software Engineering, vol. 18, no. 9, pp. 794-804, Sept. 1992, doi:10.1109/32.159837
Usage of this product signifies your acceptance of the Terms of Use.