Compositional construction and analysis of Petri net systems
Rojas, Isabel C.
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.