Verification of resource controller processes

Ramamritham, Krithivasan (1987) Verification of resource controller processes Information Systems, 12 (1). pp. 57-67. ISSN 0306-4379

Full text not available from this repository.

Official URL:

Related URL:


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.

Item Type:Article
Source:Copyright of this article belongs to Elsevier Science.
ID Code:62887
Deposited On:24 Sep 2011 05:08
Last Modified:24 Sep 2011 05:08

Repository Staff Only: item control page