Incremental specification and analysis in the context of coloured Petri nets

Incremental development involves creating a new specification or implementation by modifying an existing one. This is a commonly used technique for handling complex systems in hardware and software engineering. In fact, incremental development is fundamental to object-orientation, the widely adopted approach to software engineering which uses the mechanism of inheritance. Incremental development and object-orientation have been adopted for all phases of software engineering, from analysis to design and implementation. In the domain of concurrent systems, some researchers constrain incremental development by proposing requirements that must hold between the original and incrementally modified components. Such proposals are commonly based on a process algebra correctness relation, or require that a bisimulation relation hold between the original and modified components. In Part I of this thesis we provide background on constraining incremental change and survey several existing proposals. We identify a number of problems typical of these proposals which commonly limit their practical use. We then present Incremental Coloured Petri Net Modelling which is aimed at addressing these problems. The main contribution of this part of the thesis is the identification of these problems and the assessment of the practical applicability of Incremental Coloured Petri Net Modelling. This assessment is made by examining several case studies published in the literature. One of the primary benefits of using a formal method such as Coloured Petri Nets (CPNs) is its support for formal reasoning. State space analysis is a popular formal reasoning technique, but it is subject to state space explosion, where its application to real world models leads to unmanageably large state spaces. In Part II of this thesis we first review existing approaches for alleviating the state space explosion problem. The main contribution of Part II is a new approach, which we call Incremental Analysis. Incremental Analysis involves algorithms which take advantage of Incremental CPN Modelling in attempting to alleviate the state space explosion problem. The thesis considers the implementation issues for these algorithms, identifies the situations under which they can be expected to lead to performance improvement, and presents case studies which demonstrate the value of the technique.