A method of verification in design: an operating system case study
conference contributionposted on 2009-02-02, 14:41 authored by John A. Keane, Walter HussakWalter Hussak
This 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.
- Computer Science
CitationKEANE, J.A. and HUSSAK, W., 2000. IN: Proceedings, IEEE Annual Hawaii International Conference on System Sciences. HICSS-33, 4-7 January 2000, Vol 1
- VoR (Version of Record)
NotesThis is a conference paper [© IEEE]. It is also available from: http://ieeexplore.ieee.org/xpl/RecentCon.jsp?punumber=6709. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.