Specifying and proving properties of sentinel processes

Ramamritham , Krithivasan ; Keller, Robert M. (1981) Specifying and proving properties of sentinel processes Proceedings of the 5th IEEE international conference on Software engineering . pp. 374-382.

Full text not available from this repository.


This paper presents a technique for specifying and verifying properties of “sentinels”—a high-level language construct for synchronizing access to shared resources. Statements in the specification language possess formal temporal semantics. As a prelude to proving the correctness of sentinels, the semantics of constructs used in sentinels is given. The proof technique involves showing that the temporal behavior of a sentinel conforms to that defined by the specification. The methodology is illustrated by applying it to a typical synchronization problem.

Item Type:Article
Source:Copyright of this article belongs to IEEE Press.
ID Code:94362
Deposited On:05 Sep 2012 09:05
Last Modified:05 Sep 2012 09:05

Repository Staff Only: item control page