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

Author

Keane, John A. ; Hussak, Walter

Author_Institution

Dept. of Comput., Univ. of Manchester Inst. of Sci. & Technol., UK

fYear

2000

fDate

4-7 Jan. 2000

Abstract

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.

Keywords

formal verification; high level synthesis; operating systems (computers); temporal logic; theorem proving; 2-sorted first order temporal language; PTL theorem prover; formal verification; high-level design phase; high-level designs; manageable formal proof; operating system; operating system store manager; proportional temporal logic; Computer aided software engineering; Computer science; Concurrent computing; Costs; Hardware; Logic design; Operating systems; Programming; Software engineering; System testing;

fLanguage

English

Publisher

ieee

Conference_Titel

System Sciences, 2000. Proceedings of the 33rd Annual Hawaii International Conference on

Print_ISBN

0-7695-0493-0

Type

conf

DOI

10.1109/HICSS.2000.926971

Filename

926971