Skip to main content

Modeling Safety-Critical Systems with Z and Petri Nets

  • Conference paper
  • First Online:
Computer Safety, Reliability and Security (SAFECOMP 1999)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1698))

Included in the following conference series:

Abstract

We show how to combine the specification notation Z with Petri nets for modeling safety-critical systems. The combination preserves the strengths of the two formalisms, while ameliorating their drawbacks. We illustrate our approach by modeling a part of a production cell and validating that model with respect to safety-related properties.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [BDG+ 96]_ R. Büssow, H. Dörr, R. Geisler, W. Grieskamp, and M. Klar. μ SZ-ein Ansatz zur systematischen Verbindung von Z und Statecharts. Technical Report TR 96-32, Technische Universität Berlin, 1996.

    Google Scholar 

  2. E. Best and B. Grahlmann. PEP-more than a Petri net tool. In Proceedings TACAS’96, LNCS 1055, pages 397–401. Springer-Verlag, 1996.

    Google Scholar 

  3. R. Büssow, W. Grieskamp, W. Heicking, and S. Herrmann. An open environment for the integration of heterogeneous modelling techniques and tools. In Current Trends in Applied Formal Methods. Springer-Verlag, 1998. to appear.

    Google Scholar 

  4. M. Heiner, P. Deussen, and J. Spranger. A case study in developing control software of manufacturing systems with hierarchical Petri nets. Int. Journal of Advanced Manufacturing Technology, 15:139–152, 1999.

    Article  Google Scholar 

  5. [HLN+ 90]_ D. Harel, H. Lachover, A. Naamad, A. Pnueli, M. Politi, R. Sherman, A. Shtull-Trauring, and M. rakhtenbrot. Statemate:A working environment for the development of complex reactive systems. IEEE Transactions on Software Engineering, 16 No. 4, April 1990.

    Google Scholar 

  6. M. Heisel and C. Sühl. Formal specification of safety-critical software with Z and real-time CSP. In E. Schoitsch, editor, Proceedings 15th International Conference on Computer Safety, Reliability and Security (SAFECOMP), pages 31–45. Springer-Verlag London, 1996.

    Google Scholar 

  7. K. Jensen. Coloured Petri Nets, Basic Concepts, Analysis Methods and Practical Use, Vol. 1. Springer-Verlag, 1992.

    Google Scholar 

  8. Kolyang, T. Santen, and B. Wolff. A structure preserving encoding of Z in Isabelle/ HOL. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher-Order Logics, LNCS 1125, pages 283–298. Springer-Verlag, 1996.

    Google Scholar 

  9. C. Lewerentz and T. Lindner, editors. Formal Development of Reactive Systems. LNCS 891. Springer-Verlag, 1995.

    MATH  Google Scholar 

  10. N. Lévy and J. Souquiéres. A “Coming and Going” Approach to Specification Construction: a Scenario. In W. Schäfer, J. Kramer, and A. Wolf, editors, Proc. 8th Int. Workshop on Software Specification and Design, pages 115–118. IEEE Computer Society Press, 1996.

    Google Scholar 

  11. T. Menzel. Entwurf und Prototypimplementierung eines Petri-Netz-Framework. Technical report, BTU Cottbus, Institut für Informatik, 1997.

    Google Scholar 

  12. M. Saaltink. The Z/EVES system. In J. Bowen, M. Hinchey, and D. Till, editors, ZUM’97: The Z Formal Specification Notation, LNCS 1212, pages 72–88. Springer-Verlag, 1997.

    Chapter  Google Scholar 

  13. J. M. Spivey. The fuzz manual. Computing Science Consultancy, Oxford, 1992.

    Google Scholar 

  14. J. M. Spivey. The Z Notation-A Reference Manual. Prentice Hall, 2nd edition, 1992.

    Google Scholar 

  15. P. H. Starke and S. Roch. INA-Integrated Net Analyser version 1.7. Technical report, Humboldt-Universität Berlin, 1997.

    Google Scholar 

  16. P. H. Starke. Analyse von Petri-Netz-Modellen. Teubner, 1990.

    Google Scholar 

  17. R. Tiedemann. PED-Hierarchischer Petri-Netz-Editor. Technical report, BTU Cottbus, Institut für Informatik, 1997.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Heiner, M., Heisel, M. (1999). Modeling Safety-Critical Systems with Z and Petri Nets. In: Felici, M., Kanoun, K. (eds) Computer Safety, Reliability and Security. SAFECOMP 1999. Lecture Notes in Computer Science, vol 1698. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48249-0_31

Download citation

  • DOI: https://doi.org/10.1007/3-540-48249-0_31

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66488-8

  • Online ISBN: 978-3-540-48249-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics