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
Citation
KEANE, J.A. and HUSSAK, W., 2000. IN: Proceedings, IEEE Annual Hawaii International Conference on System Sciences. HICSS-33, 4-7 January 2000, Vol 1Publisher
© IEEEVersion
- VoR (Version of Record)
Publication date
2000Notes
This 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.ISBN
0769504930Language
- en