Hussak_Temporal_analysis_of_a_microkernel.pdf (454.78 kB)
0/0

Temporal analysis of a microkernel

Download (454.78 kB)
journal contribution
posted on 04.02.2009 by Walter Hussak
Temporal logic techniques have been proposed as a way of achieving a very natural transition from informal requirements to a formal specification of the requirements. The paper presents a case study of a real-life system developed using such techniques. Both a top-level specification and implementation semantics are given in temporal logic. In particular, the progression from statements in English to temporal logic is highlighted. A correctness proof that the implemented system satisfies the specification has been produced.

History

School

  • Science

Department

  • Computer Science

Citation

HUSSAK, W., 1995. Temporal analysis of a microkernel. Software Engineering Journal, 10 (1), pp. 21-26

Publisher

© IEEE

Version

VoR (Version of Record)

Publication date

1995

Notes

This article was published online in the journal, Software Engineering Journal [© IEEE]. It is also available at: http://ieeexplore.ieee.org/ 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.

ISSN

0268-6961

Language

en

Exports

Logo branding

Keyword(s)

Exports