Process Abstraction in the Verification of Temporal Properties

Abstract

The automatic verification of temporal properties of systems usually suffers from two problems. First, the size of the system that can be verified is very limited. Secondly, the results reflect only the behaviour of a system having particular parameters and initial conditions. Both problems are addressed by abstracting the system model relative to the property of interest. This thesis investigates two abstraction methods for processes.

In the first method unary process operators serve as abstraction operations. We show that an abstract process satisfies a property expressed as a temporal logic formula just if the original process satisfies a transformed formula. We define various abstraction operators and illustrate their use in verification with examples. The method is also used to derive two well-known verification techniques.

In the second method an abstract process and the original process are related by a process preorder. The weakly simulates and ready simulates preorders are used. For both we provide logical characterisations, abstraction operations, and algebraic laws.

Our work differs from existing work on process abstraction in that we abstract process expressions directly and take account of the particular property to be verified. We show the practical value of our methods by using them to help verify properties of Dekker's mutual exclusion algorithm and Ben-Ari's concurrent garbage collection algorithm.