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.
Abstract
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
