January 2003
The increasing pervasiveness and complexity of IT systems has lead to the unfortunate situation where IT systems are both becoming more critical for everyday life and more difficult to construct. This has lead to the development of a number of formal methods, which are mathematically based methods for specifying and reasoning about systems.
An important class of formal methods is state space methods. The basic idea underlying state space methods--at least in the most basic form--is to algorithmically calculate all the reachable states of a system and check these for desired or undesired properties. An important advantage of state space methods is that they allow most of the underlying mathematics to be hidden inside supporting computer tools, which makes state space methods highly automatic and easy to use. The main disadvantage of using state space methods is the state explosion problem: even relatively simple systems may have an astronomical, or even infinite, number of reachable states, precluding an exhaustive enumeration of the reachable states.
A number of reduction methods have been developed to alleviate the state explosion problem, and in this thesis we describe the sweep-line method, a newly developed reduction method. The basic idea underlying the sweep-line method is, when calculating the state space, to recognise and delete states that are not reachable from the currently unprocessed states. Intuitively we drag a sweep-line through the state space with the invariant that all states behind the sweep-line have been processed and are unreachable from the states in front of the sweep-line. When calculating the state space of a system we iteratively calculate successors of new states, and we need to distinguish between previously seen states and truly new states to avoid reprocessing the same states indefinitely. When calculating the successors of the known unprocessed states, all successors are in front of the sweep-line. Consequently, the states behind the sweep-line are not needed for distinguishing between new and old states and can therefore be deleted.
The thesis consists of two parts: Part I gives an overview of the sweep-line method while Part II consists of eight individual papers on different aspects of the sweep-line method. Four of these papers have been published as conference papers, one has been published as a workshop paper, while the remaining are unpublished.
Individual chapters:
Full dissertation: