Hussak_A_Method_of_Verifcation_in_Design.pdf (237.98 kB)
Download file

A method of verification in design: an operating system case study

Download (237.98 kB)
conference contribution
posted on 02.02.2009, 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.

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 1

Publisher

© IEEE

Version

VoR (Version of Record)

Publication date

2000

Notes

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

0769504930

Language

en