Process algebra is a purely symbolic formalism which is particularly well
suited
for computer manipulation.
This thesis focuses on ACP-style process algebra.
A process-algebraic specification of a concurrent system describes
the dynamic behavior of the system in a compact way while abstracting
away
from the details of its states.
The basic analysis technique in ACP-style process algebra is equational
reasoning.
The second 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.
The first activity focuses on describing the dynamic behavior
of the system under consideration.
In the second activity, a complete Petri-net model of the system is
created,
which usually contains more detail than the behavioral specification.
Third, simulation can be used to validate the Petri-net model and the
behavioral
specification of the system.
Finally, algebraic verification is used to prove formally that the
Petri-net model
satisfies the behavioral specification.
This thesis mainly focuses on the second and fourth activity of the above
method. To allow component-based design of
concurrent systems, the formalism of
modular P/T nets is introduced.
The operational semantics of modular P/T nets is formalized in a process
algebra
specifically developed for this purpose.
The theory of this thesis makes it is possible to verify, by means of
equational reasoning, the behavior of a modular P/T net against
a behavioral specification.
Two case studies are described to validate the design method and the
underlying theory in practical design situations. The main conclusion is
that Petri nets and process algebra complement each other very well, but
that the method and theory are not yet mature.
A further extension of the theory as well as the development of tool
support
is a prerequisite for successful practical applications.
The third 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.
In process algebra, these two notions correspond to the well-investigated
concepts of encapsulation and abstraction, respectively.
Four inheritance relations for dynamic behavior are defined and
studied in a simple process algebra.
The definitions and results are translated to a framework based on
labeled P/T nets,
which is a framework much closer to existing object-oriented methods
than the algebraic framework.
In the P/T-net framework, a set of transformation rules is developed
that can be used to construct classes inheriting the life cycle of
another class.
A small case study shows that these transformation rules are useful in
structuring
the design process and that they stimulate the reuse of life-cycle
specifications.
The main conclusion of the third part of this thesis is that it can be
inspiring
to study a single topic in two different formalisms.
The formalization of inheritance of dynamic behavior in process algebra
provides a clear understanding of the concept, whereas the formalization
in Petri nets yields a framework close to practice.
However, one important challenge remains, namely the integration of the
notion
of inheritance developed in this thesis in a full-fledged object-oriented
design
method.
Summarizing, it may be concluded that this thesis contributes to a better
understanding of the strengths and weaknesses of Petri nets and process
algebra.
The concepts developed in this thesis appear to be sound and promising,
although it is not yet clear to what extent the results will stimulate
the use
of formal methods in design practice.
Complete thesis:
(compressed postscript (630 kb) /
pdf (1.3 Mb))
Back to the list of publications.