Verification of resource controller processes

Abstract

Shared resources and the processes that control them play a critical role in the functioning of concurrent systems. A shared resource is viewed as an abstract data type consisting of the definition of the resource and the operations on it, with additional synchronization constraints. Here we present a technique for verifying resource controllers using the formalism of temporal logic. Properties of the operations on a given shared resource are first verified. This is followed by the verification of invariant and liveness properties of the controller. The technique is illustrated by its application to resource controller tasks in Ada. As a prerequisite for accomplishing this, we specify the semantics of Ada tasking primitives.