2134/4168
Walter Hussak
Walter
Hussak
Temporal analysis of a microkernel
Loughborough University
2009
untagged
Information and Computing Sciences not elsewhere classified
2009-02-04 12:40:50
Journal contribution
https://repository.lboro.ac.uk/articles/journal_contribution/Temporal_analysis_of_a_microkernel/9402617
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.