This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Proving Properties of Real-Time Systems Through Logical Specifications and Petri Net Models
February 1994 (vol. 20 no. 2)
pp. 127-141

Addresses the problem of formally analyzing the properties of real-time 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 Pascal-like language. The method is also illustrated through an example.

[1] M. Abadi and L. Lamport, "An Old-Fashioned Recipe for Real Time," inReal-Time: Theory in Practice, J.W. de Bakker et al., eds., Springer-Verlag, Berlin and Heidelberg, LNCS 600, 1992, pp. 1-27
[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, C. Courcoubetis, and D. Dill, "Model-checking for real-time systems," inProc. 5th Annual IEEE Symp. Logic in Computer Science, pp. 414-425, 1990.
[4] R. Alur and D. Dill, "Automata for modeling real-time systems," inProc. ICALP'91, pp. 323-335, 1991.
[5] K. R. Apt, "Ten years of Hoare's-logic: A survey--Part one,"ACM Trans. Program. Lang. Syst., vol. 3, pp. 431-483, 1981.
[6] B. Auernheimer and R. A. Kemmerer, "RT-ASLAN: A specification language for real time systems,"IEEE Trans. Software Eng., vol. SE-12, pp. 879-889, 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. 259-273, Mar. 1991.
[9] D. Bjorner and S. Prehn, "Software engineering aspects of VDM, the Vienna development method,"Theory and Practice Software Technol., pp. 85-134, 1983.
[10] C. Chang, H. Huang, and C. C. Song, "An approach to verifying concurrency behavior of real-time systems based on time Petri net and temporal logic," inProc. InfoJapan 90, pp. 307-314, 1990.
[11] 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.
[12] A. Coen, R. Kemmerer, and D. Mandrioli, "A formal framework for ASTRAL intra-level proof obligations," inProc. ESEC'93, Garmisch, Germany, pp. 483-499, 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. 181-207, 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 real-time systems through logical specifications and Petri nets models," Diparimento di Elettronica e Informazione, Politecnico di Milano, Tech. Rep. TR 91-072, Dec. 1991.
[16] M. Felder and A. Morzenti, "Validating real-time systems by executing logic specifications in TRIO," inProc 14th Int. Conf. Software Engineering, pp. 199-211, 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. 28-39, June 1993.
[18] A. Gabrielian and M. Franklin,"Multilevel specification of real-time systems,"Comm. of ACM 34, pp. 51-60, May 1991.
[19] H. Genrich, "Predicate/transition nets," inAdvances in Petri Nets, W. Reisig and G. Rozemberg, Eds. Berlin-New York: Springer, 1987, pp. 109-136.
[20] R. Gerber and I. Lee, "A layered approach to automating the verification of real-time systems,"IEEE Trans. Software Eng., vol. 18, no. 9, pp. 768-784, 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 19-20, 1989. Washington, DC: IEEE Computer Society Press, 1989.
[22] C. Ghezzi, D. Mandrioli, and A. Morzenti, "TRIO: A logic language for executable specifications of real-time systems,"J. Systems Software, vol. 12, pp. 107-123, 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 high-level Petri net model for time-critical systems,"IEEE Trans. Software Eng., vol. 17, no. 2, pp. 60-172, Feb. 1991.
[25] C. Ghezzi and R. Kemmerer, "ASTRAL: An assertion language for specifying real-time systems," inProc. 3rd European Software Engineering Conf., Milan, Italy, pp. 122-146, Oct. 1991.
[26] T. A. Henziger, Z. Manna, and A. Pnueli, "Temporal proof methodologies for real-time systems," inProc. 18th ACM Symp. Principles of Programming Languages, pp. 353-366, 1991.
[27] T. Henzinger, Z. Manna, and A. Pnueli, "Timed transitions systems," inReal Time: Theory and Practice. New York: Springer, pp. 226-251, 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 real-time systems,"IEEE Trans. Software Eng., vol. SE-12, no. 9, pp. 890-904, Sept. 1986.
[30] F. Jahanian, R. S. Lee, and A. K. Mok, "Semantics of Modechart in real-time 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. Real-Time Systems Symp., Huntsville, AL, 1988.
[32] K. Jensen, "Coloured Petri nets," in Advances in Petri Nets, W. Reisig and G. Rozemberg, Eds. Berlin-New York: Springer, 1987.
[33] R. A. Kemmerer, "Testing formal specifications to detect design errors,"IEEE Trans. Software Eng., vol. 11, no. 1, pp. 32-43, Jan. 1985.
[34] Y. Kesten and A. Pnueli, "Timed and hybrid Statecharts and their textual representation," inProc. School on Formal Techniques in Real-Time and Fault-Tolerant Systems, Nijmegen, Netherlands, Jan. 1992.
[35] R. Koymans, "Specifying real-time properties with metric temporal logic,"Real-Time Systems, vol. 2, no. 4, pp. 255-299, 1990.
[36] F. Kröger, "Temporal logic of programs," inEATCS Monographs on Theoretical Computer Science. New York: Springer-Verlag, 1987.
[37] J. C. Laprie, N. B. Levenson, E. Pilaud, and M. Thomas, "Panel 2: Real-life safety-critical software," in12th Int. Conf. on Software Engineering, ICSE'90, pp. 222-229, 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. SE-13, no. 3, pp. 386-397, Mar. 1987.
[39] P. Merlin and D.J. Faber, "Recoverability of communication protocols,"IEEE Trans. Commun, vol. COM-24, 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. 39-58, July 1991.
[41] A. Morzenti, D. Mandrioli, and C. Ghezzi, "A model parametric real-time logic,"ACM Trans. Programming Languages and Systems, vol. 14, no. 4, pp. 521-573, Oct. 1992.
[42] J. Ostroff,Temporal Logic of Real-Time 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, Springer-Verlag, N.Y., 1986, pp. 510-584.
[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. 440-449, 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: Springer-Verlag, 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. 1273-1281, Nov. 1990.
[49] H. Tuominen, "Proving properties of elementary net systems with a special-purpose theorem prover," inProc. Workshop on Automatic Verification Methods for Finite State Systems, pp. 97-104, 1989.
[50] J. Wing, "A specifier's introduction to formal methods,"IEEE Comput., vol. 23, no. 9, pp. 8-24, Sept. 1990.

Index Terms:
real-time systems; temporal logic; Petri nets; formal specification; theorem proving; real-time systems; property proving; logical specifications; TRIO; formal analysis; timed Petri net; temporal logic; axiomatization; Hoare method; embedded systems; first-order logic; formal specification; dual language
Citation:
M. Felder, D. Mandrioli, A. Morzenti, "Proving Properties of Real-Time Systems Through Logical Specifications and Petri Net Models," IEEE Transactions on Software Engineering, vol. 20, no. 2, pp. 127-141, Feb. 1994, doi:10.1109/32.265634
Usage of this product signifies your acceptance of the Terms of Use.