
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
M. Felder, D. Mandrioli, A. Morzenti, "Proving Properties of RealTime Systems Through Logical Specifications and Petri Net Models," IEEE Transactions on Software Engineering, vol. 20, no. 2, pp. 127141, February, 1994.  
BibTex  x  
@article{ 10.1109/32.265634, author = {M. Felder and D. Mandrioli and A. Morzenti}, title = {Proving Properties of RealTime Systems Through Logical Specifications and Petri Net Models}, journal ={IEEE Transactions on Software Engineering}, volume = {20}, number = {2}, issn = {00985589}, year = {1994}, pages = {127141}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.265634}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Proving Properties of RealTime Systems Through Logical Specifications and Petri Net Models IS  2 SN  00985589 SP127 EP141 EPD  127141 A1  M. Felder, A1  D. Mandrioli, A1  A. Morzenti, PY  1994 KW  realtime systems; temporal logic; Petri nets; formal specification; theorem proving; realtime systems; property proving; logical specifications; TRIO; formal analysis; timed Petri net; temporal logic; axiomatization; Hoare method; embedded systems; firstorder logic; formal specification; dual language VL  20 JA  IEEE Transactions on Software Engineering ER   
Addresses the problem of formally analyzing the properties of realtime systems. We propose a method based on modeling the system as a timed Petri net and on specifying its properties in TRIO, an extension of temporal logic suitable for dealing explicitly with time and for measuring it. Timed Petri nets are axiomatized in terms of TRIO, so that their properties can be derived as theorems in the same spirit as the classical Hoare method allows one to prove properties of programs coded in a Pascallike language. The method is also illustrated through an example.
[1] M. Abadi and L. Lamport, "An OldFashioned Recipe for Real Time," inRealTime: Theory in Practice, J.W. de Bakker et al., eds., SpringerVerlag, Berlin and Heidelberg, LNCS 600, 1992, pp. 127
[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, C. Courcoubetis, and D. Dill, "Modelchecking for realtime systems," inProc. 5th Annual IEEE Symp. Logic in Computer Science, pp. 414425, 1990.
[4] R. Alur and D. Dill, "Automata for modeling realtime systems," inProc. ICALP'91, pp. 323335, 1991.
[5] K. R. Apt, "Ten years of Hoare'slogic: A surveyPart one,"ACM Trans. Program. Lang. Syst., vol. 3, pp. 431483, 1981.
[6] B. Auernheimer and R. A. Kemmerer, "RTASLAN: A specification language for real time systems,"IEEE Trans. Software Eng., vol. SE12, pp. 879889, Sept. 1986.
[7] G. Berry and L. Cosserat, "The ESTEREL synchronous programming language and its mathematical semantics," inProc. CMU Seminar on Concurrency, LNCS 185. New York: Springer, 1990.
[8] B. Berthomieu and M. Diaz, "Modeling and verification of time dependent systems using time Petri nets,"IEEE Trans. Software Eng., vol. 17, no. 3, pp. 259273, Mar. 1991.
[9] D. Bjorner and S. Prehn, "Software engineering aspects of VDM, the Vienna development method,"Theory and Practice Software Technol., pp. 85134, 1983.
[10] C. Chang, H. Huang, and C. C. Song, "An approach to verifying concurrency behavior of realtime systems based on time Petri net and temporal logic," inProc. InfoJapan 90, pp. 307314, 1990.
[11] 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.
[12] A. Coen, R. Kemmerer, and D. Mandrioli, "A formal framework for ASTRAL intralevel proof obligations," inProc. ESEC'93, Garmisch, Germany, pp. 483499, Sept. 1983.
[13] W. Damm, G. Dohmen, V. Gerstner, and B. Josko, "Modular verification of Petri nets, the temporal logic approach," inProc. Stepwise Refinement of Distributed Systems. Models, Formalisms, Correctness, LNCS 430. New York: Springer, pp. 181207, 1990.
[14] H. B. Enderton,A Mathematical Introduction to Logic. New York: Academic, 1972.
[15] M. Felder, D. Mandrioli, and A. Morzenti, "Proving properties of realtime systems through logical specifications and Petri nets models," Diparimento di Elettronica e Informazione, Politecnico di Milano, Tech. Rep. TR 91072, Dec. 1991.
[16] M. Felder and A. Morzenti, "Validating realtime systems by executing logic specifications in TRIO," inProc 14th Int. Conf. Software Engineering, pp. 199211, May 1992.
[17] M. Felder, C. Ghezzi, and M. Pezzé, "Analyzing refinements of state based specifications: The case of TB nets," inProc, ISSTA'93, Cambridge, England, pp. 2839, June 1993.
[18] A. Gabrielian and M. Franklin,"Multilevel specification of realtime systems,"Comm. of ACM 34, pp. 5160, May 1991.
[19] H. Genrich, "Predicate/transition nets," inAdvances in Petri Nets, W. Reisig and G. Rozemberg, Eds. BerlinNew York: Springer, 1987, pp. 109136.
[20] R. Gerber and I. Lee, "A layered approach to automating the verification of realtime systems,"IEEE Trans. Software Eng., vol. 18, no. 9, pp. 768784, Sept. 1992.
[21] C. Ghezzi, D. Mandrioli, S. Morasca and M. Pezzè, "A general way to put time in Petri nets," inProc. 5th Int. Workshop Software Specifications and Design, Pittsburgh, PA, May 1920, 1989. Washington, DC: IEEE Computer Society Press, 1989.
[22] C. Ghezzi, D. Mandrioli, and A. Morzenti, "TRIO: A logic language for executable specifications of realtime systems,"J. Systems Software, vol. 12, pp. 107123, 1990.
[23] C. Ghezzi, M. Jazayeri, and D. Mandrioli,Fundamentals of Software Engineering. Englewood Cliffs, NJ: Prentice, 1991.
[24] C. Ghezzi, D. Mandrioli, S. Morasca, and M. Pezzè"A unified highlevel Petri net model for timecritical systems,"IEEE Trans. Software Eng., vol. 17, no. 2, pp. 60172, Feb. 1991.
[25] C. Ghezzi and R. Kemmerer, "ASTRAL: An assertion language for specifying realtime systems," inProc. 3rd European Software Engineering Conf., Milan, Italy, pp. 122146, Oct. 1991.
[26] T. A. Henziger, Z. Manna, and A. Pnueli, "Temporal proof methodologies for realtime systems," inProc. 18th ACM Symp. Principles of Programming Languages, pp. 353366, 1991.
[27] T. Henzinger, Z. Manna, and A. Pnueli, "Timed transitions systems," inReal Time: Theory and Practice. New York: Springer, pp. 226251, 1991.
[28] T. Henzinger, "Sooner is safer than later," Stanford Univ., Tech. Rep., 1991.
[29] F. Jahanian and A. K. Mok, "Safety analysis of timing properties in realtime systems,"IEEE Trans. Software Eng., vol. SE12, no. 9, pp. 890904, Sept. 1986.
[30] F. Jahanian, R. S. Lee, and A. K. Mok, "Semantics of Modechart in realtime logic," inProc. 21st Hawaii Int. Conf. Syst. Sci., Jan. 1988.
[31] F. Jahanian and D. Stuart, "A method for verifying properties of Modechart specifications," inProc. RealTime Systems Symp., Huntsville, AL, 1988.
[32] K. Jensen, "Coloured Petri nets," in Advances in Petri Nets, W. Reisig and G. Rozemberg, Eds. BerlinNew York: Springer, 1987.
[33] R. A. Kemmerer, "Testing formal specifications to detect design errors,"IEEE Trans. Software Eng., vol. 11, no. 1, pp. 3243, Jan. 1985.
[34] Y. Kesten and A. Pnueli, "Timed and hybrid Statecharts and their textual representation," inProc. School on Formal Techniques in RealTime and FaultTolerant Systems, Nijmegen, Netherlands, Jan. 1992.
[35] R. Koymans, "Specifying realtime properties with metric temporal logic,"RealTime Systems, vol. 2, no. 4, pp. 255299, 1990.
[36] F. Kröger, "Temporal logic of programs," inEATCS Monographs on Theoretical Computer Science. New York: SpringerVerlag, 1987.
[37] J. C. Laprie, N. B. Levenson, E. Pilaud, and M. Thomas, "Panel 2: Reallife safetycritical software," in12th Int. Conf. on Software Engineering, ICSE'90, pp. 222229, 1990. See also Panel 3: Industrial experience with formal methods, organized by D. Bjorner and L. Druffel.
[38] N.G. Leveson and J.L. Stolzy, "Safety analysis using Petri nets,"IEEE Trans. Software Eng., vol. SE13, no. 3, pp. 386397, Mar. 1987.
[39] P. Merlin and D.J. Faber, "Recoverability of communication protocols,"IEEE Trans. Commun, vol. COM24, no. 9, Sept. 1976.
[40] A. Morzenti and P. San Pietro, "An object oriented logic language for modular system specification," inProc. European Conf. Object Oriented Programming 91, Geneva, pp. 3958, July 1991.
[41] A. Morzenti, D. Mandrioli, and C. Ghezzi, "A model parametric realtime logic,"ACM Trans. Programming Languages and Systems, vol. 14, no. 4, pp. 521573, Oct. 1992.
[42] J. Ostroff,Temporal Logic of RealTime Systems. Research Studies Press, 1990.
[43] A. Pnueli, "Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of CurrentTrends," inCurrent Trends in Concurrency: Overviews and Tutorials. W.P. de Roever and G. Rozenberg, eds., Lecture Notes in Computer Science 224, SpringerVerlag, N.Y., 1986, pp. 510584.
[44] C. V. Ramamoorthy and G. S. Ho, "Performance evaluation of asynchronous concurrent systems using Petri nets,"IEEE Trans. Software Eng., vol. 6, no. 9, pp. 440449, Sept. 1980.
[45] C. Ramchandani, "Analysis of asynchronous concurrent systems by timed Petri nets," Massachusetts Inst. Technol., Project MAC, Tech. Rep. 120, Feb. 1974.
[46] W. Reisig, "Petri nets: An introduction," inEATCS Monographs on Theoretical Computer Science. New York: SpringerVerlag, 1985.
[47] J. M. Spivey,The Z Notation: A Reference Manual (Computer Science Series). Englewood Cliffs, NJ: Prentice Hall International, 1989.
[48] I. Suzuki, "Formal analysis of alternating bit protocol by temporal Petri nets,"IEEE Trans. Software Eng., vol. 16, no. 11, pp. 12731281, Nov. 1990.
[49] H. Tuominen, "Proving properties of elementary net systems with a specialpurpose theorem prover," inProc. Workshop on Automatic Verification Methods for Finite State Systems, pp. 97104, 1989.
[50] J. Wing, "A specifier's introduction to formal methods,"IEEE Comput., vol. 23, no. 9, pp. 824, Sept. 1990.