Abstract
Our approach of rule-based refinement1provides a formal description for the stepwise system development based on Petri nets. Rules with a left-hand and a right-hand side allow replacing subnets in a given algebraic high-level net system. The extension of these rules supports the preservation of system properties. In this paper we extend the preservation of safety properties significantly. We define rules, that introduce new safety properties. In our new approach we propose first the verification of properties at the moment they can be expressed and then their preservation further on. Hence, properties can be checked as long as the system is still small. Moreover, introducing properties allows checking these for the relevant subpart only. Changes that are required later on can be treated the same way and hence preserve the system properties. Hence, we have made a step towards a formal technique for the stepwise system development during analysis and design.
This paper continues our research on rule-based refinement of algebraic high-level nets, we have first introduced at FASE 98 [PGE98].
Chapter PDF
Keywords
References
W. Deiters and V. Gruhn. Process Management in Practice-Applying the FunSoft Net Approach to Large-Scale Processes. Automated Software Engineering, 5:7–25, 1998.
H. Ehrig, M. Gajewsky, and F. Parisi-Presicce. High-Level Replacement Systems with Applications to Algebraic Specifications and Petri Nets, volume 3: Concurrency, Parallelism, and Distribution, chapter 6, pages 341–400. World Scientific, Handbook of Graph Grammars and Computing by Graph Transformations edition, 1999.
H. Ehrig, A. Habel, H.-J. Kreowski, and F. Parisi-Presicce. Parallelism and concurrency in High Level Replacement Systems. Math. Struc. in Comp. Science, 1:361–404, 1991.
H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 1: Equations and Initial Semantics, volume 6 of EATCS Monographs on Theoretical Computer Science. Berlin, 1985.
C. Ermel. Anforderungsanalyse eines medizinischen Informationssystems mit Algebraischen High-Level-Netzen. Technical Report 96-15, TU Berlin, 1996.
Maike Gajewsky, Julia Padberg, and Kathrin Hoffmann. Safety Introducing and Preserving Rules for Algebraic High-Level Net Systems. Technical report, Technical University Berlin, 2000. to appear.
V. Gruhn. Validation and Verification of Software Process Models. PhD thesis, Universität Dortmund, Abteilung Informatik, 1991.
K. Jensen, S. Christensen, P. Huber, and M. Holla. Design/CPN. A Reference 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: Basic Concepts. Springer Verlag, EATCS Monographs in Theoretical Computer Science edition, 1992.
K. Jensen and G. Rozenberg, editors. High-Level Petri-Nets: Theory and Application. 1991.
J. Meseguer and U. Montanari. Petri Nets are Monoids. Information and Computation, 88(2):105–155, 1990.
Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems, Specification. 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 Refinement. PhD thesis, Technical University Berlin, 1996. Shaker Verlag.
Julia Padberg. Categorical Approach to Horizontal Structuring and Refinement of High-Level Replacement Systems. Applied Categorical Structures, 7(4):371–403, December 1999.
J. Padberg, H. Ehrig, and L. Ribeiro. Algebraic high-level net transformation systems. Mathematical Structures in Computer Science, 5:217–256, 1995.
J. Padberg, M. Gajewsky, and C. Ermel. Rule-Based Refinement of High-Level Nets Preserving Safety Properties. In E. Astesiano, editor, Fundamental approaches to Software Engineering, pages 221–238, 1998. Lecture Notes in Computer Science 1382.
W. Reisig. Petri Nets, volume 4 of EATCS Monographs on Theoretical Computer Science. 1985.
J. Vautherin. Parallel System Specification with Coloured Petri Nets. In G. Rozenberg, editor, Advances in Petri Nets 87, pages 293–308, 1987. 266.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Padberg, J., Hoffmann, K., Gajewsky, M. (2000). Stepwise Introduction and Preservation of Safety Properties in Algebraic High-Level Net Systems. In: Maibaum, T. (eds) Fundamental Approaches to Software Engineering. FASE 2000. Lecture Notes in Computer Science, vol 1783. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46428-X_18
Download citation
DOI: https://doi.org/10.1007/3-540-46428-X_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67261-6
Online ISBN: 978-3-540-46428-0
eBook Packages: Springer Book Archive