Compositional construction and analysis of Petri net systems

                       Isabel C. Rojas M.



Most Petri net (PN) based modelling formalisms represent
the system modelled as a flat net. This may not clearly reflect the
elements that participate in the system and the way they communicate
or interact. It can also be difficult to determine the model's
behaviour or prove some of its properties. Viewing the model as a
set of components that interact is more appropriate, especially for
models of parallel and distributed systems.
 
In this thesis a compositional method for the construction and
analysis of Well-formed nets (WNs) systems is presented.  WNs allow
a natural representation of complex distributed systems, maintaining
the same expressive power as the unconstrained coloured net
formalisms.  The main motivation of this work has been to offer an
appropriate method for the   specification, design and analysis of 
parallel and distributed systems. The set of composition operations 
defined is based on the operators of Process Algebras (PA).  Mimicking 
the PA operators allows us to benefit from the compositional nature of 
PA. The definition of the composition operations has taken into account 
the peculiarities and characteristics of the PN formalisms, such as
synchronisation, state evolution and token flow. The models obtained by
applying the compositional method proposed are termed compositional WN
cWN) systems.

To consolidate a framework for the compositional construction and
analysis of cWNs, we study the construction of structural and
state space information about a cWN using information about its
sub-components. The matrix description of the
model---known as the incidence matrix---is shown to be obtainable using the
incidence matrices of its sub-components, together  with the knowledge
of the composition operations used.  By studying the
relation between the resulting incidence matrix and the incidence
matrices of its sub-components, methods are proposed to obtain the
semiflows of the cWN model, using the semiflows of its
sub-components.  New, higher-level semiflows are defined, based on
the structured definition of colours and arc functions of WN
models.

We show how the state space of a higher-level component can be built
from the state spaces of its sub-components. This leads to the
definition of a grouping of markings, termed a composed
marking. It is proved that state space analysis over composed
markings allows the verification of state space properties of the
complete system, such as reachability, absence of deadlock and
liveness, using the reduced state space.

The concepts and propositions introduced are illustrated throughout
the dissertation by the use of a series of examples. The methods
proposed are applied over a model of a flexible manufacturing
system, as a way to consolidate the understanding of the
methodology.
  
As a step towards the definition of a methodology for the
performance oriented compositional construction and analysis of
Stochastic Well-formed net systems modelling parallel and
distributed systems, we study the extension of the compositional
operations and methods proposed to support the incorporation of time
specifications of the system modelled.