Weakest Congruences, Fairness and Compositional Process-Algebraic Verification

Abstract

Traditionally, computer programs have been thought of as entities which take some input, execute a sequence of statements that process this input, and then return the result. More recently, concurrent and reactive computer systems have become increasingly important. Concurrency means that the system consists of several independent, interacting components, and reactiveness means that the system is capable of continuous and simultaneous communication in several directions. Examples of concurrency and reactiveness can be found in operating systems, embedded systems, computer networks and mobile communication.

Designing concurrent and reactive systems is difficult and error-prone. This is because the existence of concurrent components usually enables an enormous number of possible sequences of events in the system, and the complex communication patterns of reactive behaviour can be difficult to specify and analyse. It is hoped that concurrent and reactive systems can be made more reliable if we use precise mathematical models to represent these systems, and develop methods and computer tools for analysing their behaviour through these models.

Process algebra is one approach for modelling concurrent and reactive systems. In the process-algebraic model the system components make progress by executing actions, which are indivisible, atomic units with identity. Communication between concurrent entities is based on executing common actions synchronously. An important advantage offered by this approach is compositionality, which means that different components of a system can be considered in isolation and described by the behaviour that can be observed at their interface. This makes it possible to replace one component with another, simpler and smaller component that behaves in an equivalent way, which reduces the complexity of the overall system model.

However, we must first have a precisely defined notion of equivalent behaviour. A behavioural equivalence must support compositionality, that is, it must be a congruence, and it should not make unnecessary distinctions between systems, that is, it should be as weak as possible. Here we identify weakest congruences related to the progress properties of systems, namely, to livelocks and deadlocks.

Another issue related to progress is fairness. This means that even though a system is allowed to make individual choices freely, it is not allowed to constantly favour some choices at the expense of others. We investigate how fairness can be used to guarantee progress in a compositional setting.

Sometimes compositionality makes it possible to handle arbitrarily large systems by using invariants that guarantee that the behaviour of a system stays the same when we add any number of certain components. As an example, we present a case study in which invariants are used to show that the external behaviour of a communication protocol is independent of the capacities of the underlying channels.