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.