Name
Abstract | ||
|---|---|---|
This paper reports a study of verification in the high-level design phase of operating system development in which both rigorous and formal verification are used, where the rigorous argument is used to determine a manageable formal proof to be carried out. A 2-sorted first order temporal language is used to express several possible high-level designs and the required properties of an operating system store manager. The case of large system limits is reduced to a case of small system limits by use of a rigorous argument. Corresponding propositional temporal logic (PTL) formulae are then verified using a PTL theorem prover. |
Year | Venue | Keywords |
|---|---|---|
2000 | HICSS | rigorous argument,corresponding propositional temporal logic,small system limit,operating system store manager,high-level design phase,system development,large system limit,manageable formal proof,ptl theorem prover,formal verification |
Field | DocType | ISBN |
Propositional temporal logic,First order,Computer science,Automated theorem proving,Store manager,Theoretical computer science,Formal verification,Formal proof | Conference | 0-7695-0493-0 |
Citations | PageRank | References |
0 | 0.34 | 0 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| J. A. Keane | 1 | 96 | 7.33 |
| W | 2 | 0 | 0.34 |
| Hussak | 3 | 0 | 0.34 |