Name
Abstract | ||
|---|---|---|
An implementation in Pascal by Saxena and Bredt of the Monitor construct is studied. Techniques are given for using a program verifer to analyse the conditions under which the implementation is fair (i.e. once a process is delayed it eventually will be continued). By use of a virtual data structure, fairness is represented in terms of simple properties which can be verified automatically.
Examples are given illustrating how the verification can force unstated assumptions upon which the implementation depends to be made explicit, and how it can be used to study whether the implementation makes adequate use of resources. The development of techniques for analysis of such implementations is required before the correctness of high-level language operating systems such as Brinch Hansen's SOLO can be completely established.
|
Year | Venue | Keywords |
|---|---|---|
1976 | ICSE | virtual data structure,brinch hansen,adequate use,program verifer,simple property,high-level language operating system,unstated assumption,verification,data structure,condition variables,operating system,high level language |
Field | DocType | ISBN |
Data structure,Programming language,Computer science,Correctness,Implementation,Real-time computing,Monitor | Conference | 978-0-89791-146-7 |
Citations | PageRank | References |
4 | 2.04 | 2 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Richard Alan Karp | 1 | 14 | 6.47 |
| David C. Luckham | 2 | 731 | 393.69 |