Abstract

In Terms of Nets

System Design with Petri Nets and Process Algebra

To date, there are many different formal methods for describing and analyzing concurrent systems. Two of the most widely used formalisms are Petri nets and process algebra. The main motivation of this thesis is to study topics combining these two formalisms. One part of this thesis combines Petri nets and process algebra in a method supporting the compositional design of concurrent systems. The method consists of four activities, namely behavioral specification, Petri-net modeling, simulation, and algebraic verification. Two case studies are described to validate the design method in practical design situations. Another part of this thesis describes an approach to inheritance of dynamic behavior. Most object-oriented design methods currently used in practice contain a more or less precise definition of inheritance for the attributes and methods of classes. However, they lack a definition of inheritance for object life cycles that describe the dynamic behavior of objects. This thesis formalizes inheritance of dynamic behavior both in a process-algebraic setting and in a Petri- net framework. In the chosen approach, blocking and hiding method calls play a crucial role. A small case study shows that the concepts developed in this thesis are useful in structuring the design process and that they stimulate the reuse of life-cycle specifications. This thesis contributes to a better understanding of the strengths and weaknesses of Petri nets and process algebra. The results appear to be sound and promising, although it is not yet clear to what extent they will stimulate the use of formal methods in design practice.