Integration of specification for modeling and specification for system design

  • Chang-Yu Wang
  • Kishor S. Trivedi
Full Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 691)


This paper presents a procedure of transforming an Estelle specification into Stochastic Reward Net(SRN) formalism. Estelle is an ISO standard formal specification language which can help avoid ambiguity, incompleteness and inconsistency in system development. SRN is a well-developed modeling technique that is used to carry out performance and reliability analysis. Integration of specification for system design like Estelle and specification for modeling like SRN can minimize the effort and the cost in designing a functionally correct as well as reliable and performance satisfied system. The objective of transforming Estelle into SRN is to have a system designer specify a system using Estelle and then the specification is automatically transformed into SRN to carry out the performance and reliability analysis.


Interaction Point Data Frame System Task Message Type Firing Time 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    M. Ajmone Marsan and G. Chiola. On Petri nets with deterministic and exponentially distributed firing times. In Lecture Notes in Computer Science, volume 266, pages 132–145. Springer-Verlag, 1987.Google Scholar
  2. 2.
    M. Ajmone Marsan, G. Conte, and G. Balbo. A class of generalized stochastic Petri nets for the performance evaluation of multiprocessor systems. ACM Transactions on Computer systems, 2:93–122, 1984.Google Scholar
  3. 3.
    D. Aldous and L. Shepp. The least variable phase type distribution is Erlang. Stochastic Models, 3(3):467–473, 1987.Google Scholar
  4. 4.
    S. Budkowski and P. Dembinski. An introduction of Estelle: A specification language for distributed systems. Computer Networks and ISDN Systems, 14:3–23, 1987.Google Scholar
  5. 5.
    G. Chiola. A grpahical Petri net tool for performance analysis. In S. Fdida and G. Pujolle, editors, Modeling Techniques and Performance Evaluation, pages 323–333, 1987.Google Scholar
  6. 6.
    H. Choi, V. G. Kulkarni, and K. S. Trivedi. Markov Regenerative Stochastic Petri Nets. Technical Report DUKE-CCSR-93-001, Center for Computer Systems Research, Duke University, 1993.Google Scholar
  7. 7.
    H. Choi, V. G. Kulkarni, and K. S. Trivedi. Transient analysis of deterministic and stochastic Petri nets. In Proceedings of The 14th International Conference on Application and Theory of Petri Nets, Chicago, U.S.A., Jun. 21–25 1993.Google Scholar
  8. 8.
    G. Ciardo, A. Blakemore, P.F. Chimento, JR., J.K. Muppala, and K.S. Trivedi. Automated generation and analysis of Markov reward models using Stochastic Reward Nets. In C. Meyer and R.J. Plemmons, editors, Linear Algebra, Markov Chains, and Queueing Models, Heidelberg, 1992. Springer-Verlag.Google Scholar
  9. 9.
    G. Ciardo, J. Muppala, and K.S. Trivedi. Analyzing concurrent and fault-tolerant software using stochastic reward nets. Journal of Parallel and Distributed Computing, pages 255–269, 1992.Google Scholar
  10. 10.
    G. Ciardo, J.K. Muppala, and K.S. Trivedi. Manual for the SPNP Package. Department of Electrical Engineering, Duke University, Sept. 1991.Google Scholar
  11. 11.
    J. P. Courtiat, A. Pedroza, and J.M. Ayache. A simulation environment for protocol specifications described in Estelle. In M. Diaz, editor, IFIP WG 6.1 6th International Workshop on Protocol Specification, Testing and Verification. North-Holland, 1986.Google Scholar
  12. 12.
    A. Cumani. ESP — a package for the evaluation of stochastic Petri nets with phase-type distributed transition times. In Proceedings of the International Workshop on Timed Petri Nets, Torino Italy, July 1985.Google Scholar
  13. 13.
    P. Dembinski and S. Budkowski. Simulating Estelle specifications with time parameters. In H. Rudin and C. H. West, editors, IFIP WG 6.1 7th International Workshop on Protocol Specification, Testing and Verification. North-Holland, 1987.Google Scholar
  14. 14.
    J. Bechta Dugan, K.S. Trivedi, V. Nicola, and R. Geist. Extended stochastic petri nets: Applications and analysis. In E. Gelenbe, editor, Performance '84, pages 507–519. North-Holland, 1985.Google Scholar
  15. 15.
    O. C. Ibe, H. Choi, and K. S. Trivedi. Performance evaluation of client-server systems. IEEE Transactions on Parallel and Distributed Systems, To Appear.Google Scholar
  16. 16.
    O.C. Ibe, K.S. Trivedi, A. Sathaye, and R.C. Howe. Stochastic Petri net modeling of VAXcluster system availability. In Proceedings of the International Conference on Petri Nets and Performance Models, Kyoto, Japan, Dec. 1989.Google Scholar
  17. 17.
    ISO. Information Processing — Open System Interconnection-Estelle: A formal description technique based on an extended state transition model. ISO International Standard 9074, 1988.Google Scholar
  18. 18.
    M. Malhotra, 1992. Personal communication, Computer Science Dept., Duke University.Google Scholar
  19. 19.
    M.K. Molly. Performance analysis using stochastic Petri nets. IEEE Transactions on Computers, C-31:913–917, 1982.Google Scholar
  20. 20.
    J.K. Muppala, S. Woolet, and K.S. Trivedi. Real-time systems performance in the presence of failures. IEEE computer, May 1991.Google Scholar
  21. 21.
    J.L.Peterson. Petri Net Theory and the Modeling of Systems. Prentice-Hall, 1981.Google Scholar
  22. 22.
    Richard J. Linn, Jr. The features and facilities of Estelle. In M. Diaz, editor, IFIP WG 6.1 5th International Workshop on Protocol Specification, Testing and Verification, pages 271–296. North-Holland, 1985.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Chang-Yu Wang
    • 1
  • Kishor S. Trivedi
    • 2
  1. 1.Department of Computer ScienceDuke UniversityDurham
  2. 2.Department of Electrical Eng.Duke UniversityDurham

Personalised recommendations