Temporal analysis of a microkernel
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-26Publisher
© IEEEVersion
- VoR (Version of Record)
Publication date
1995Notes
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-6961Language
- en
