University of Tasmania
whole_LewisGlennAnthony2002_thesis.pdf (14.71 MB)

Incremental specification and analysis in the context of coloured Petri nets

Download (14.71 MB)
posted on 2023-05-26, 17:53 authored by Lewis, GA
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.


Publication status

  • Unpublished

Rights statement

Copyright 2002 the author - The University is continuing to endeavour to trace the copyright owner(s) and in the meantime this item has been reproduced here in good faith. We would be pleased to hear from the copyright owner(s). Thesis (PhD)--University of Tasmania, 2002. Includes bibliographical references

Repository Status

  • Open

Usage metrics

    Thesis collection


    No categories selected



    Ref. manager