State Space Methods for Coloured Petri Nets

Abstract

An increasing number of system development projects are concerned with distributed and concurrent systems. There are numerous examples, ranging from large scale systems, in the areas of telecommunication and applications based on WWW technology, to medium or small scale systems, in the area of embedded systems. A typical distributed or concurrent system consists of a number of independent but communicating processes. This means that the execution of such systems may proceed in many different ways, e.g., depending on whether messages are lost, the speed of the processes involved, and the time at which input is received from the environment. As a result, distributed and concurrent systems are, by nature, complex and difficult to design and test. This has motivated the development of methods which support computer-aided analysis, validation, and verification of the behaviour of concurrent and distributed systems.
State space methods are some of the most prominent approaches in this field. The basic idea underlying state spaces is (in its simplest form) to compute all reachable states and state changes of the system, and represent these as a directed graph. The virtue of a constructed state space is that it makes it possible to algorithmically reason about the behaviour of a system, e.g., verify that the system possesses certain desired properties or locate errors in the system. The main disadvantage of using state spaces is the state explosion problem: even relatively small descriptions/systems may have an astronomically or even infinite number of reachable states, and it is a serious limitation on the use of state space methods in the analysis of real-life systems. The development of reduction methods to alleviate this inherent complexity problem is, therefore, a central topic in the development of state space methods. Reduction methods avoid representing the entire state space of the system or represent the state space in a compact form. The reduction is done in such a way that properties of the system can still be derived from the reduced state space.
In this thesis we study state space methods in the framework of Coloured Petri Nets which is a graphical language for modelling and analysis of concurrent and distributed systems. The thesis consists of two parts. Part I is the mandatory overview paper which summarises the work which has been done. Part II is composed of five individual papers and constitutes the core of this thesis. Four of the these papers have been published elsewhere as conference papers, journal papers, or book chapters.
The overview paper introduces the research field of state space methods for Coloured Petri Nets and summarises the contents and contributions of the five individual papers. A substantial part of the overview paper has also been devoted to putting the results presented in the five individual papers in a broader perspective in the form of a discussion of related work.
The first paper considers state space analysis of Coloured Petri Nets. It is well-known that almost all dynamic properties of the considered system can be verified when the state space is finite. However, state space analysis is more than just formulating a set of formal requirements and invoking a corresponding set of queries. State space analysis is also applicable during the design and debugging of a system. An approach towards this is to allow the user to analyse the behaviour of systems by drawing and generating selected parts of the state space. The paper presents a tool in which formal verification, partial state spaces, and analysis by means of graphical feedback and simulation are integrated entities. The focus of the paper is twofold: the support for graphical feedback and the way it has been integrated with simulation, and the underlying algorithms and datastructures which support computation and storage of state spaces and which exploit the hierarchical structure of the models.
The second paper presents a computer tool for verification of distributed systems. The tool implements the method of state spaces with symmetries. The basic idea in the approach is to exploit the symmetries inherent in many distributed systems in order to construct a condensed state space. As an example, the correctness of Lamport's Fast Mutual Exclusion Algorithm is established. We demonstrate a significant increase in the number of states which can be analysed. State spaces with symmetries is not our invention. Our contribution is the development of the tool and verification of the example, demonstrating how the method of state spaces with symmetries can be put into practical use.
The third paper demonstrates the potential of verification based on state spaces reduced by equivalence relations. The basic observation is that quite often some states of a system are similar, i.e., they induce similar behaviours. Similarity can be formally expressed by defining an equivalence relation on the set of states and on the set of actions of a system under consideration. A state space can be constructed in which the nodes correspond to equivalence classes of states, and the arcs correspond to equivalence classes of actions. Such a state space is often much smaller than the ordinary, full state space, but it does allow derivation of many verification results. State spaces with equivalence classes is not our invention. The contribution of the paper is the specification of a concrete notion of equivalence, and a demonstration of its application for verification of a communication protocol. Aided by a developed computer tool significant reductions of state spaces are exhibited, representing some first results on the practical use of state spaces with equivalence classes for Coloured Petri Nets. Exploiting the symmetries in systems induce a certain kind of equivalence. The verification of the communication protocol demonstrates the potential provided by more general notions of equivalence.
The fourth paper addresses the issue of using the stubborn set method for Coloured Petri Nets without relying on unfolding to the equivalent Place/Transition Net. The stubborn set method exploits the independence between actions to avoid representing all possible interleavings of the system execution. We give a lower bound result which states that there exist Coloured Petri Nets for which computing good stubborn sets requires time proportional to the size of the equivalent Place/Transition Net. We suggest an approximative method for computing stubborn sets of so-called process-partitioned Coloured Petri Nets which does not rely on unfolding. The underlying idea is to add some structure to the Coloured Petri Net, which can be exploited during the stubborn set construction to avoid the unfolding. The practical applicability of the method is demonstrated with both theoretical and experimental case studies, in which reduction of the state space, as well as savings in time, are obtained.
The fifth paper presents two new question-guided stubborn set methods for state properties. The first method makes it possible to determine whether a state is reachable in which a given state property holds. It generalises earlier results on stubborn sets for state properties in the sense that the earlier methods can be seen as an implementation of our more general method. We also propose alternative, more powerful implementations that have the potential of leading to better reduction results. This potential is demonstrated on some practical case studies. As an extension of the first method, we present a novel method which can be used to determine if it is always possible to reach a state where a given state property holds. Compared to earlier methods the benefit is again in the potential for better reduction results. omputer-aided analysis, validation, and verification of the behaviour of concurrent and distributed systems.