In: Lecture Notes in Computer Science, Vol. 1382: Fundamental Approaches to Software Engineering, pages 221-238. Springer-Verlag, 1998.
Also in: Science of Computer Programming, Vol. 39, No. 1, pages 97-118. 2001.
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 structuring 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 requirement analysis of a medical information system. The main new result in this paper extends rule-based modification of algebraic high-level 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.
Keywords: high-level Petri nets, rule-based refinements, safety properties, temporal logic, vertical net structuring.