The derivation of performance expressions for communication protocols from timed petri net models

ABSTRACT

Petri Net models have been extended in a variety of ways and have been used to prove the correctness and evaluate the performance of communication protocols. Several extensions have been proposed to model time. This work uses a form of Timed Petri Nets and presents a technique for symbolically deriving expressions, which describe system performance. Unlike past work on performance evaluation of Petri Nets which assumes a priori knowledge of specific time delays, the technique presented here applies to a wide range of time delays so long as the delays satisfy a set of timing constraints. The technique is demonstrated using a simple communication protocol.

REFERENCES

• 1: Berthomieu, B., and M. Menasche, "An Enumerative Approach for Analyzing Time Petri Nets" Proceedings of the 1983 IFIP Congress, Paris, (Sept. 1983).
• 2: Gérard Berthelot , Richard Terrat, Petri Nets Theory for the Correctness of Protocols, Proceedings of the IFIP WG6.1 Second International Workshop on Protocol Specification, Testing and Verification, p.325-342, May 17-20, 1982
• 3: Bochmann, G.V., "A General Transition Model of Protocols and Communication Services," IEEE Transactions on Communication COM-28,4 (April 1980), pp. 645-650.
• 4: Coolahan, J.E., and N. Roussopoulos, "Timing Requirements for Time-Driven Systems Using Augmented Petri Nets" IEEE Transactions on Software Engineering, SE-9,5 (Sept. 1983), pp. 603-616.
• 5: Hailpern, B. and S. Owicki, "Verifying Network Protocols Using Temporal Logic", Proceedings of Trends and Applications Symposium, 1980, Computer Network Protocols National Bureau of Standards, Maryland, (May 1980).
• 6: Merlin, P. and D. Farber, "A Methodology for the Design and Implementation of Communications Protocols," IEEE Transactions on Communications, COM-24, 6 (June 1976).
• 7: Molloy, M. "On the Integration of Delay and Throughput Measures in Distributed Processing Models", Computer Science Dept., University of California, Los Angeles, Report No. CSD-810921, September 1981.
• 8: Razouk, R.R., and G. Estrin "Modeling and Verification of Communication Protocols: The X.21 Interface" IEEE Transactions on Computers, C-29,12 (December 1980), pp. 1038-1052.
• 9: Ramamoorthy C.V. and G.S. Ho, "Performance Evaluation of Asynchronous Concurrency Systems using Petri Nets," IEEE Transactions on Software Engineering, SE-6, 5 (September 1980), 440-449.
• 10: C. Ramchandani, ANALYSIS OF ASYNCHRONOUS CONCURRENT SYSTEMS BY TIMED PETRI NETS, Massachusetts Institute of Technology, Cambridge, MA, 1974
• 11: Razouk, R.R., and C. Phelps "Performance Analysis Using Timed Petri Nets", Tech. Rept. 206, University of California, Irvine, (1983). (Submitted to 4th Int. Conf. on Distributed Computing Systems, May 1984).
• 12: Krishan K. Sabnani , Mischa Schwartz, Verification of a Multidestination Protocol Using Temporal Logic, Proceedings of the IFIP WG6.1 Second International Workshop on Protocol Specification, Testing and Verification, p.21-41, May 17-20, 1982
• 13: Joseph Sifakis, Use of Petri Nets for Performance Evaluation, Proceedings of the Third International Symposium on Measuring, Modelling and Evaluating Computer Systems, p.75-93, October 03-05, 1977
• 14: Gerald A. Simon , David J. Kaufman, An Extended Finite State Machine Approach to Protocol Specification, Proceedings of the IFIP WG6.1 Second International Workshop on Protocol Specification, Testing and Verification, p.113-133, May 17-20, 1982
• 15: Symons, F.J.W., "Verification of Communication Protocols using Numerical Petri Nets," Australian Telecommunication Research, 14,1 (1980) 34-38.
• 16: Teng, A.Y., and M.T. Liu, "A Formal Approach to the Design and Implementation of Network Communication Protocol," Proceedings of COMPSAC, (May 1980), pp. 722-727.
• 17: Mary K. Vernon , Edmundo de Souza e Silva , Gerald Estrin, Performance Evaluation of Asynchronous Concurrent Systems: The UCLA Graph Model of Behavior, Proceedings of the 9th International Symposium on Computer Performance Modelling, Measurement and Evaluation, p.153-171, May 25-27, 1983
• 18: Lawrence Yelowitz , Susan L. Gerhart , G. Hilborn, Modeling a Network Protocol in AFFIRM and Ada, Proceedings of the IFIP WG6.1 Second International Workshop on Protocol Specification, Testing and Verification, p.435-450, May 17-20, 1982
• 19: W. M. Zuberek, Timed Petri nets and preliminary performance evaluation, Proceedings of the 7th annual symposium on Computer Architecture, p.88-96, May 06-08, 1980, La Baule, United States [doi>10.1145/800053.801913]

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.4 PERFORMANCE OF SYSTEMS

Additional Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.2 Network Protocols
          Subjects: Protocol verification

  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Petri nets
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

General Terms:
Design, Performance, Verification