
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
X. Nicollin, J. Sifakis, S. Yovine, "Compiling RealTime Specifications into Extended Automata," IEEE Transactions on Software Engineering, vol. 18, no. 9, pp. 794804, September, 1992.  
BibTex  x  
@article{ 10.1109/32.159837, author = {X. Nicollin and J. Sifakis and S. Yovine}, title = {Compiling RealTime Specifications into Extended Automata}, journal ={IEEE Transactions on Software Engineering}, volume = {18}, number = {9}, issn = {00985589}, year = {1992}, pages = {794804}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.159837}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Compiling RealTime Specifications into Extended Automata IS  9 SN  00985589 SP794 EP804 EPD  794804 A1  X. Nicollin, A1  J. Sifakis, A1  S. Yovine, PY  1992 KW  realtime specifications; realtime systems; extended automata; simple specification language; communicating processes; timeout; watchdog constructs; timed automata; state variables; eventdriven execution mode; complexity; efficient code generation; symbolic modelchecking; realtime properties; automata theory; communicating sequential processes; formal specification; program compilers; realtime systems; specification languages VL  18 JA  IEEE Transactions on Software Engineering ER   
A method for the implementation and analysis of realtime 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 eventdriven 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 modelchecking of realtime properties can be directly applied to this model.
[1] R. Alur, C. Courcoubetis, and D. Dill, "Modelchecking for realtime systems," inProc. 5th Annual IEEE Symp. Logic in Computer Science, pp. 414425, 1990.
[2] R. Alur and T. Henzinger, "A really temporal logic," inProc. 30th Symp. Foundations of Computer Science, pp. 164169, IEEE Computer Society Press, 1989.
[3] R. Alur and T. Henzinger, "Logics and models of realtime: A survey," inProc. REX Workshop RealTime: Theory in Practice, Lecture Notes in Computer Science 600, SpringerVerlag, The Netherlands, June 1991.
[4] R. Alur, "Techniques for automatic verification of realtime 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: AddisonWesley, 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, SpringerVerlag, 1985.
[7] J. B. Burchet al., "Symbolic model checking: 1020states and beyond," inProc. 5th Symp. Logics in Computer Science, pp. 428439, IEEE Computer Society Press, 1990.
[8] E. M. Clarke, E. A. Emerson, and A. P. Sistla, "Automatic verification of finitestate concurrent systems using temporal logic,"ACM Trans. Program. Lang. Syst., vol. 8, no. 2, pp. 244263, 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 branchingtime temporal logic," inProc. Workshop Logic of Programs, Lecture Notes in Computer Science 131, SpringerVerlag, 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. 231274, 1987.
[15] T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, "Symbolic modelchecking for realtime 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 graphtheoretic approach for timing analysis and its implementation,"IEEE Trans. Comput., vol. 36, pp. 961975, 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. RTC26, LG1IMAG, 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 ComputerAided Verification, Denmark, July 1991.
[24] X. Nicollin, J. Sifakis, and S. Yovine, "From ATP to timed graphs and hybrid systems," inProc. REX Workshop "RealTime: Theory in Practice,"Lecture Notes in Computer Science 600, SpringerVerlag, The Netherlands, June 1991.
[25] J. Ostroff,Temporal Logic of RealTime Systems. Research Studies Press, 1990.
[26] J. Parrow, "Verifying a CSMA/CDprotocol 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 realtime systems," inProc. Formal Techniques in RealTime and FaultTolerant Systems (LNCS 331), pp. 8498, 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: PrenticeHall, 1981.
[30] S. Yovine, "Graph of timers: An approach to translate ATP into timed graphs,"Tech. Rep., LGIIMAG, France, Sept. 1991.