Verification of co-operating systems and behaviour abstraction

Checking the design or specification of a co-operating, i.e. concurrent and reactive, system for correctness is an important task in the development of complex - we call them industrial-sized - systems. Applying the well-established approach of automatic verification of specifications using model checking techniques, one is confronted with severe complexity problems when verifying large systems. The source of these complexity problems is the excessive size of the state-space that represents the behaviour of a specification as well as the necessity of exhaustively searching the state-space when model checking. The obvious aim when dealing with complex systems is to reduce the state-space as much as possible without loss of important information concerning the actual verification task. We show in this thesis which information about the behaviour of a specification can be obtained from properties of a simplified version of the behaviour. The step from the original behaviour - we call it the concrete behaviour - of a specification to its simplified version is called abstraction. The behaviour of a specification is represented by the minimal state-space corresponding to the specification, which in fact means, that we do not consider additional state information, but only the behaviour itself, i.e. infinite sequences of actions. For this reason we call our abstraction technique behaviour abstraction. In formal terms, we define an abstraction by an alphabetic language homomorphism. Alphabetic language homomorphisms offer two abstraction concepts: action renaming and action hiding. It is especially the fact that we deal with abstractions that comprise action hiding that makes our approach quite powerful with regard to the aim of obtaining a small finite state representation of the abstract behaviour. The application area of the concepts we develop in this thesis is the area of co-operating systems. These are loosely coupled reactive concurrent systems. For this type of system it is often not sufficient to check a property without making any fairness assumptions. On the other hand, dealing with fairness is not an easy task in the sense that one has to make the right choice which fairness assumption to take into account. To be freed from explicitly looking at fairness issues we define in this thesis a relativized version of liveness: relative liveness. A relative liveness property is a liveness property with respect to the universe of a specification's behaviour. Relative liveness is also known as machine-closure. The use of relative liveness properties in verification of co-operating systems using behaviour abstraction proves to be somewhat delicate. Arbitrary alphabetic language homomorphisms are not an adequate basis for abstraction when one wants to check relative liveness properties. We show that the definition of a homomorphism that is simple on a behaviour is exactly the right choice to establish an abstraction technique that preserves relative liveness properties. Based on this result, we show additionally for another class of properties, eventuality properties, that they, too, are preserved under simple homomorphic abstractions. Finally we apply the results of this thesis to three different examples that are chosen to illustrate different aspects of the established results. One of the examples has a concrete practically relevant background: it shows how the established approach can be used to detect service interactions in intelligent networks