Time in state based formal description techniques for distributed systems

  • Jp. Courtiat
  • M. Diaz
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 600)


Formal Approaches have been recognized to be of high importance for designing communication and cooperation protocols. They provide unambiguous descriptions, support validation analyses and allow assessment of the conformance of implementations against specifications. This paper presents how some mature and important techniques based on extensions of state machines are able to handle in an integrated way functional and time requirements. It is in particular shown how Time Petri net models can be combined together with the Estelle Formal Description Technique to define Estelle*, a very powerful language for describing highly dynamic and time dependent hierarchies of communicating architectures.


Distributed Systems Specification FDTs Formal Description Techniques Verification Manipulating Explicit Time values Time Petri nets Estelle Integrating Time Petri nets and Estelle 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [AKY]
    I. F. AKYILDIZ, G. CHIOLA, D. KOFMAN, H. KOEREZLIOKLU, “Stochastic Petri net Modeling of the FDDI Network Protocol”, Int Symp on Protocol Specification, Verification and Testing, IFIP PSTV XI, Stockholm, June 1991, North-Holland, B. Pershon et al Editors.Google Scholar
  2. [BUD]
    S. BUDKOWSKI, P. DEMBINSKI, “An introduction to Estelle: a specification language for distributed systems”, Computer Networks and ISDN Systems, 14, 1987, pp 3–23.CrossRefGoogle Scholar
  3. [COU2]
    J.-P. COURTIAT, “Estelle and Petri Nets: A Petri Net based Semantics for Estelle — Introducing a Rendez-Vous mechanism in Estelle: Estelle*” in [Diaz 89].Google Scholar
  4. [COU3]
    J.-P. COURTIAT, P. de SAQUI-SANNES, “ESTIM: an integrated environment for the simulation and verification of OSI protocols specified in Estelle*”, Special Issue of the Journal of Computer Networks and ISDN Systems on Tools for Protocol Engineering, to appear, end of 1991.Google Scholar
  5. [DES]
    P. DE SAQUI-SANNES, J.P. COURTIAT, “From the Simulation to the Verification of Estelle Specifications”, 2nd International Conference on Formal Description Techniques (FORTE 89), S.T. Vuong Editor, North-Holland, 1990.Google Scholar
  6. [DES1]
    P. DE SAQUI-SANNES, J.P. COURTIAT, “An extension of the Multi-way synchronization mechanism concealed by Estelle”, Int Symp on Protocol Specification, Verification and Testing, IFIP PSTV XI, Stockholm, June 1991, North-Holland.Google Scholar
  7. [DIA]
    M. DIAZ, “Modeling and analysis of communication and cooperation protocols using Petri net based models”, Tutorial paper, Computer Networks, vol.6, n∘ 6, December 1982.Google Scholar
  8. [DIA1]
    M. DIAZ, J.P. ANSART, J.P. COURTIAT, P. AZEMA, V. CHARI, Editors, “The Formal description techniques Estelle”, North-Holland, 1989.Google Scholar
  9. [DIA2]
    M. DIAZ, C.A. VISSERS, “SEDOS, Software environment for the design of open distributed systems”, IEEE Software Magazine, November 1989.Google Scholar
  10. [DIA3]
    M. Diaz, J. Dufau, R. Groz, Experiences using Estelle within SEDOS-Estelle-Demonstrator, 2nd Int Conf on Formal Description Techniques, FORTE 89, Vancouver, December 1989, North Holland.Google Scholar
  11. [DEM]
    P. Dembinski, S. Budkowski, “Simulating Estelle Specifications with Time Parameters”, Int. Symp. on Protocol Specification, Testing and Verification, IFIP PSTV VII, Zurich, May 1987, North-Holland.Google Scholar
  12. [DUG]
    J. DUGAN, K. TRIVEDI, R. GEIST, V. NICOLA, “Extended stochastic Petri nets applications and analysis”, Performance 84, December 1984.Google Scholar
  13. [GEN]
    H.J GENRICH, K. LAUTENBACH, “The Analysis of Distributed Systems by means of Predicate/ Transition Nets” in Lecture Notes on Computer Science, Springer Verlag, 1979.Google Scholar
  14. [HOL]
    M.A. Holliday, M.K. Vernon, “A generalized timed Petri net model for performance analysis”, IEEE Trans. on Software Engineering, vol. SE-13, n∘12, December 1987, pp. 1297–1310.Google Scholar
  15. [ISO1]
    ISO-IS9074.ISO/TC97/SC21/WG1-FDT/SC-B, “Estelle, a formal description technique based on an extended state transition model”, 1989.Google Scholar
  16. [ISO2]
    ISO-IS9074,ISO/TC97/SC21/WG1-FDT/SC-C, “LOTOS, a formal description technique based on an extended state transition model”, 1989.Google Scholar
  17. [JON]
    N.D. JONES, L.H. LANDWEBER, Y.E. LIEN, “Complexity of some problems in Petri nets”, Theoretical Computer Science 4, 1977.Google Scholar
  18. [JUA1]
    G. JUANOLE, J. L. ROUX, “On the Pertinence of Extended Time Petri Net Model for Analyzing Communication Activities”, IEEE 3rd Int Workshop on Petri Nets and Performance Models”, Kyoto, December 1989.Google Scholar
  19. [JUA2]
    G. JUANOLE, Y. ATAMNA, “Dealing with arbitrary time distributions with the Stochastic Timed Petri net model — Application to Queuing systems”, Int Conf on Petri Nets and Performance Models, Melbourne, 1991.Google Scholar
  20. [KEL]
    R. M. KELLER, “Formal Verification of Parallel Programs”, Comm. of the ACM, July 1986.Google Scholar
  21. [LAU]
    K. LAUTENBACH, H. A. SCHMID, “Use of Petri Nets for proving Correctness of Concurrent process systems”, Proc. of the IFIP Congress, North Holland, 1974.Google Scholar
  22. [MAR]
    M. A. MARSAN, G. BALBO, G. CONTE, “A Class of Generalized Stochastic Petri Nets for the Performance Evaluation of Multiprocessor System”, ACM Trans. on Comp. Syst., May 1984, pp. 93–122.Google Scholar
  23. [MAR1]
    M. A. MARSAN, G. BALBO, A. BOBBIO, G. CHIOLA, G. CONTE, A. CUMANI, “On Petri nets with stochastic timing”, Int. Workshop on Timed Petri Nets, Torino, July 1985.Google Scholar
  24. [MAZ]
    V.B. MAZZOLA, J-P. COURTIAT, M. DIAZ, A-M. DRUILHE, J-F. LENOTRE, P. MICHAUD, “Flexible Assembly Cell: an implementation using the Estelle FDT”, 6th CIM-Europe Conf., Lisboa, Portugal, May 1990.Google Scholar
  25. [MER]
    P. M. MERLIN, “A methodology for design and implementation of protocols”, IEEE Tr on Communications, June 1976.Google Scholar
  26. [MER1]
    P. M. MERLIN, D.J. FARBER, “Recoverability of communications protocols”, IEEE Trans, on Communications, September 1976.Google Scholar
  27. [MIL]
    R. MILNER, “Communication and Concurrency”, Prentice-Hall, 1989.Google Scholar
  28. [MOL]
    M. K. MOLLOY, “Performance Analyses using Stochastic Petri Nets”, IEEE Tr on Computers, September 1982.Google Scholar
  29. [NIC]
    R. de NICOLA, “Extensional equivalences for transition systems”, Acta Informatica, Vol. 24, 1987.Google Scholar
  30. [PNU]
    A. Pnueli, “Applications of Temporal Logic to Reactive Systems: a Survey of Current Trends”, LNCS, V 224, 1986.Google Scholar
  31. [11]
    C. RAMCHANDANI, “Analysis of asynchronous concurrent systems by timed Petri nets”, Project MAC, TR 120, Massachussets Institute of Technology, Feb. 1974.Google Scholar
  32. [25]
    R.R. RAZOUK, C.V. PHELPS, “Performance analysis using time Petri nets”, 4th IFIP Protocol Specification, Testing and Verification, North-Holland, 1985, Y. Yemini Ed.Google Scholar
  33. [REE1]
    G. M. REED and A. W. ROSCOE, A timed Model for Communicating Sequential Processes, volume 58, pages 249–261. North-Holland, 1988.Google Scholar
  34. [RIC]
    J. L. RICHIER, C. RODRIGUEZ, J. SIFAKIS, J. VOIRON, Verification in XESAR of the sliding window protocol, Int. Symp. on Protocol Specification, Testing and Verification, IFIP PSTV VII, North-Holland, 1987.Google Scholar
  35. [ROU]
    J. L. ROUX, G. JUANOLE, “Functional and Performance Analyses using Extended Petri Nets”, Int. Work. on Petri Nets and Performance Models, Madison-WI, August 1987.Google Scholar
  36. [SMI]
    F.D. SMITH, C.H. WEST, “Technologies for network architecture and implementation”, IBM J. of Res. and Develop., vol.27, n∘1, January 1983.Google Scholar
  37. [VAN1]
    P. VAN EIJK, C. VISSERS, M. DIAZ Editors, The Formal description technique LOTOS, North-Holland, 1989.Google Scholar
  38. [YUA]
    M.C. YUANG, “Survey of Protocol Verification Techniques Based on Finite State Models”, Proc. of the IEEE Computer Networking Symposium, Washington, April 1988.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Jp. Courtiat
    • 1
  • M. Diaz
    • 1
  1. 1.Laboratoire d'Automatique et d'Analyse des Systèmes du Centre National de la Recherche ScientifiqueToulouse CedexFrance

Personalised recommendations