This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Modeling and Verification of Time Dependent Systems Using Time Petri Nets
March 1991 (vol. 17 no. 3)
pp. 259-273

A description and analysis of concurrent systems, such as communication systems, whose behavior is dependent on explicit values of time is presented. An enumerative method is proposed in order to exhaustively validate the behavior of P. Merlin's time Petri net model, (1974). This method allows formal verification of time-dependent systems. It is applied to the specification and verification of the alternating bit protocol as a simple illustrative example.

[1] J. M. Ayache, J. P. Couriat, and M. Diaz, "REBUS, A fault-tolerant distributed system for industrial real-time control,"IEEE Trans. Comput., vol. C-31, no. 7, July 1982.
[2] K. A. Bartlett, R. A. Scantlebury, and P.T. Wilkinson, "A note on reliable full-duplex transmission over half-duplex link,"Commun. ACM, vol. 12, no. 5, May 1969.
[3] B. Berthomieu and M. Menasche, "A state enumeration approach for analyzing time Petri nets," inProc. 3rd European Workshop Applications and Theory of Petri Nets, Varenna, Italy, Sept. 1982.
[4] B. Berthomieu and M. Menasche, "An enumerative approach for analyzing time Petri nets," inProc. IFIP Cong. 1983, Paris, Sept. 1983.
[5] P. Caspi and N. Halbwachs, "Analyse approchée du comportement asymptotique de systèmes temporisés," Lab. d'Informatique et de Mathématiques Appliquées de Grenoble, Rep. RR 322, Sept. 1982 (in French).
[6] N. D. Jones, L. H. Landweber, and Y. E. Lien, "Complexity of some problems in Petri nets,"Theoret. Comput. Sci., vol. 4, 1977.
[7] R. M. Karp and R.E. Miller, "Parallel program schemata,"J. Comput. Syst. Sci., vol. 3, 1969.
[8] M. Menasche, "Analyse des réseaux de Petri temporisés et application aux systèmes distribués," Thesis, Univ. Paul Sabatier, Toulouse, France, Nov. 1982 (in French).
[9] P. Merlin and D.J. Faber, "Recoverability of communication protocols,"IEEE Trans. Commun, vol. COM-24, no. 9, Sept. 1976.
[10] P. Merlin, "A study of the recoverability of computer system," Thesis, Dep. Comput. Sci., Univ. California, Irvine, 1974.
[11] C. Ramchandani, "Analysis of asynchronous concurrent systems by timed Petri nets," Massachusetts Inst. Technol., Project MAC, Tech. Rep. 120, Feb. 1974.
[12] A. Danthine, "Protocol representation with finite-state models,"IEEE Trans. Commun., vol. COM-28, no. 4, Apr. 1980.
[13] M. Diaz, "Modeling and analysis of communication and cooperation protocols using Petri net based models,"Comput. Networks, Dec. 1982.
[14] J. Sifakis,Use of Petri Nets for Performance Evaluation in Measuring, Modelling, and Evaluating Computer Systems. Amsterdam, The Netherlands: North-Holland, 1977, pp. 75-93.
[15] W. M. Zuberek, "Timed Petri nets and preliminary performance evaluation," inProc. 7th Annu. Symp. Computer Architecture, May 6-8, 1980, pp. 88-96.
[16] P. Chretienne, "Some results on the control of timed Petri nets," inProc. 2nd Workshop Applications and Theory of Petri Nets, Bad Honnef, Sept. 1981.
[17] M. Menasche and B. Berthomieu, "Time Petri nets for analyzing and verifying time dependent communication protocols," inProtocol Specification, Testing and Verification, III, H. Rudin and C. H. West, Eds. Amsterdam, The Netherlands: North-Holland, 1983.
[18] M. Diaz and P. Azema, "Petri net based models for the specification and validation of protocols," inAdvances in Petri Nets (Lecture Notes in Computer Science, Vol. 188). New York: Springer-Verlag, 1985.
[19] P. Caspi and N. Halbwachs, "An approach to real time systems modelling," inProc. 2nd Workshop Applications and Theory of Petri Nets, Bad Honnef, Sept. 1981.
[20] G. B. Dantzig,Linear Programming and Extensions. Princeton, NJ: Princeton University Press, 1963.
[21] N. D. Jones, L. H. Landweber, and Y. E. Lien, "Complexity of some problems in Petri nets,"Theoret. Comput. Sci., vol. 4, pp. 277-299, 1977.
[22] M. Hack, "Petri net languages," Computation Structures Group, Massachusetts Inst. Technol., Project MAC, Memo 124, June 1975.
[23] R. M. Karp and R.E. Miller, "Parallel program schemata,"J. Comput. Syst. Sci., vol. 3, pp. 147-195, 1969.
[24] B. Aspvall and Y. Shiloach, "A polynomial time algorithm for solving systems of linear inequalities with two variables for inequality," inProc. 20th Annu. Symp. Foundations of Computer Sciences, Oct. 1979, pp. 205-217.
[25] R. R. Razouk and C. V. Phelps, "Performance analysis using time Petri nets," inProc. 4th IFIP Protocol Specification, Testing and Verification, Y. Yeminiet al., Eds. Amsterdam, The Netherlands: North-Holland, 1985.
[26] K. Lautenbach and H.A. Schmidt, "Use of Petri nets for proving correctness of concurrent process systems," inProc. IFIP Congr. 1974. Amsterdam, The Netherlands: North-Holland, 1974, pp. 187-191.
[27] S. Ghosh, "Some comments on timed Petri nets,"Journées sur les Réseaux de Petri, AFCET, Paris, 1977.
[28] J. Dufau, "Un outil pour la vérification des protocoles décrits par réseaux de Petri," Thèse de Docteur-Ingénieur, Univ. Paul Sabatier, Toulouse, France, Jan. 1984 (in French).
[29] M. A. Holliday and M. K. Vernon, "A generalized timed Petri net model for performance analysis,"IEEE Trans. Software Eng., vol. SE-13, no. 12, pp. 1297-1310, Dec. 1987.
[30] J. L. Roux, "Modélisation et analyse des systèmes distribués par les réseaux de Petri temporels," Thèse de Docteur-Ingénieur INSA, Toulouse, France, Dec. 1985 (in French).

Index Terms:
verification; time dependent systems; time Petri nets; concurrent systems; communication systems; explicit values; formal verification; time-dependent systems; specification; alternating bit protocol; formal specification; parallel programming; Petri nets; program verification; protocols
Citation:
B. Berthomieu, M. Diaz, "Modeling and Verification of Time Dependent Systems Using Time Petri Nets," IEEE Transactions on Software Engineering, vol. 17, no. 3, pp. 259-273, March 1991, doi:10.1109/32.75415
Usage of this product signifies your acceptance of the Terms of Use.