×

Rule-based refinement of high-level nets preserving safety properties. (English) Zbl 0969.68109

Summary: 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- 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 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.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Software:

Design/CPN
Full Text: DOI