Abstract
The concept of rule-based modification developed in the area of algebraic graph transformations and high-level replacement systems has recently shown to be a powerful concept for vertical stucturing of Petri nets. This includes low-level and high-level Petri nets, especially algebraic high-level nets which can be considered as an integration of algebraic specifications and Petri nets. In a large case study rule-based modification of algebraic high-level nets has been applied successfully for the requirements analysis of a medical information system. The main new result in this paper extends rule-based modification of algebraic highlevel nets such that it preserves safety properties formulated in terms of temporal logic. For software development based on rule-based modification of algebraic high-level nets as a vertical development strategy this extension is an important new technique. It is called rule-based refinement. As a running example an important safety property of a medical information system is considered and is shown to be preserved under rule-based refinement.
This work is part of the joint research project “DFG-Forschergruppe Petrinetz-Technologie” between H. Weber (Coordinator), H. Ehrig (both from the Technical University Berlin) and W. Reisig (Humboldt-UniversitÄt zu Berlin), supported by the German Research Council (DFG).
Chapter PDF
References
E. Best, R. Devillers, and J. Hall. The Box Calculus: a new causal algebra with multi-label communication. In Advances in Petri Nets, pages 21–69. Lecture Notes in Computer Science, 1992. 609.
W. Brauer, R. Gold, and W. Vogler. A Survey of Behaviour and Equivalence Preserving Refinements of Petri Nets. Advances in Petri Nets, LNCS 483, 1990.
J. Bradfield and C. Stirling. Verifying temporal properties of processes. In J. C. M. Baeten et al., editors, LNCS; CONCUR'90, Theories of Concurrency: Unification and Extension. (Conference, 1990, Amsterdam, The Netherlands), pages 115–125, Springer, Berlin, 1990.
F. Cornelius, H. Hu\mann, and M. Löwe. The Korso Case Study for Software Engineering with Formal Methods: A Medical Information System. In M. Broy and S. JÄhnichen, editors, KORSO: Methods, Languages, and Tools for the Construction of Correct Software, pages 417–445. Springer LNCS 1009, 1995. Also appeared as technical report 94-5, TU Berlin.
W. Damm, G. Döhmen, V. Gerstner, and B. Josko. Modular verification of petri nets: The temporal logic approach. In J. W. de Bakker et al., editors, LNCS; Proceedings of the REX Workshop on Stepwise Refinement, 1989, Mook, The Netherlands, pages 180–207, Springer, Berlin, 1990.
C. Dimitrovici, U. Hummert, and L. Petrucci. Composition and net proper-ties of algebraic high-level nets. In Advances of Petri Nets. Springer Verlag Berlin LNCS 524, 1991.
J. Desel and A. Meceron. Vincinity Respecting Net Morphisms. In Ad-vances in Petri Nets, pages 165–185. Springer Verlag LNCS 483, 1990.
C. Ermel and M. Gajewsky. Expanding the Use Of Structuring: Formal Justification for Working on Subnets. In Proceedings of Workshop Petri Nets in System Engineering '97, pages 44-54, University Hamburg, 1997. FBI-HH-B-205/97.
H. Ehrig, A. Habel, H.-J. Kreowski, and F. Parisi-Presicce. Parallelism and concurrency in high-level replacement systems. Math. Struct. in Comp. Science, 1:361–404, 1991.
H. Ehrig. Introduction to the algebraic theory of graph grammars. In V. Claus, H. Ehrig, and G. Rozenberg, editors, 1st Graph Grammar Workshop, LNCS 73, pages 1–69. Springer Verlag, 1979.
H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 1: Equa-tions and Initial Semantics, volume 6 of EATCS Monographs on Theoretical Computer Science. Springer Verlag, Berlin, 1985.
H. Ehrig and J. Padberg. Introduction to Universal Parametrized Net Classes. In H. Weber, H. Ehrig, and W. Reisig, editors, MoveOn-Proc. der DFG-Forschergruppe “Petrinetz-Technologie”, Technical Report 97-21, TU Berlin, 1997.
C. Ermel, J. Padberg, and H. Ehrig. Requirements Engineering of a Medical Information System Using Rule-Based Refinement of Petri Nets. In D. Cooke, B.J. KrÄmer, P. C-Y. Sheu, J.P. Tsai, and R. Mittermeir, editors, Proc. Integrated Design and Process Technology, pages 186–193. Society for Design and Process Science, 1996. Vol.1.
C. Ermel. Anforderungsanalyse eines medizinischen Informationssystems mit Algebraischen High-Level-Netzen. Techn. Report 96-15, TU Berlin, 1996.
H.J. Genrich. Predicate/Transition Nets. In High-Level Petri Nets: Theory and Application, pages 3–43. Springer, 1991.
R.J. van Glabbeck and U. Golz. Equivalences and Refinement. In Semantics of Systems of Concurrent Processes, pages 309–333. Springer, 1990. Lecture Notes in Computer Science 469.
H.J. Genrich and K. Lautenbach. System modelling with high-level Petri nets. Theoretical Computer Science, 13:109–136, 1981.
R. R. Howell, L. E. Rosier, and Chun Yen Hsu. A taxonomy of fairness and temporal logic problems for petri nets. Theoretical Computer Science, 82(2):341–372, 1991.
U. Hummert. Algebraische High-Level Netze. PhD thesis, Technische Uni-versitÄt Berlin, 1989.
K. Jensen, S. Christensen, P. Huber, and M. Holla. Design/CPN. A Ref-erence Manual. Meta Software Cooperation, 125 Cambridge Park Drive, Cambridge Ma 02140, USA, 1991.
K. Jensen. Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use, volume 1. Springer, 1992.
K. Jensen. Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use, volume 2. Springer, 1995.
J. Lilius. On the Structure of High-Level Nets. PhD thesis, Helsinki University of Technology, 1994.
Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems, Specification. Springer-Verlag, 1992.
A. Oberweis, G. Scherrer, and W. Stucky. INCOME/STAR: Methodology and Tools for the Development of Distributed Information Systems. Information Systems, 19(8):643–660, 1994.
J. Padberg. Abstract Petri Nets: A Uniform Approach and Rule-Based Re-finement. PhD thesis, Technical University Berlin, 1996. Shaker Verlag.
J. Padberg, H. Ehrig, and L. Ribeiro. Algebraic high-level net transforma-tion systems. Math. Struct. in Computer Science, 5:217–256, 1995.
S. Peuker. Invariant property preserving extensions of elementary petri nets. Technical Report No.97–21, TU Berlin, 1997.
J. Padberg, M. Gajewsky, and C. Ermel. Refinement versus Verification: Compatibility of Net-Invariants and Stepwise Development of High-Level Petri Nets. Technical Report 97-22, TU Berlin, 1997. to appear.
W. Reisig. Petri Nets and Algebraic Specifications. Theoretical Computer Science, 80:1–34, 1991.
K. Schmidt. Symbolische Analysemethoden für algebraische Petri-Netze, volume 4. Bertz Verlag, versal edition, 1996.
J. Svensson and M. Meier. Handbuch LEU Support-Guide. Vebacom Service GmbH. Also, http://www.lion.de/PRODUKT/produkt.html.
Vautherin, J. Parallel System Specification with Coloured Petri Nets. In Rozenberg, G., editor, Advances in Petri Nets 87, pages 293–308. LNCS 266, Springer, 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Padberg, J., Gajewsky, M., Ermel, C. (1998). Rule-based refinement of high-level nets preserving safety properties. In: Astesiano, E. (eds) Fundamental Approaches to Software Engineering. FASE 1998. Lecture Notes in Computer Science, vol 1382. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0053593
Download citation
DOI: https://doi.org/10.1007/BFb0053593
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64303-6
Online ISBN: 978-3-540-69723-7
eBook Packages: Springer Book Archive