Hussak_A_Method_of_Verifcation_in_Design.pdf (237.98 kB)
Download fileA method of verification in design: an operating system case study
conference contribution
posted on 2009-02-02, 14:41 authored by John A. Keane, Walter HussakWalter HussakThis paper reports a study of verification in the high-level design phase of operating system development in which both a 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 proportional temporal logic (PTL) formulae are then verified using a PTL theorem prover.
History
School
- Science
Department
- Computer Science