TEMPORAL ANALYSIS OF A MICROKERNEL

Temporal logic techniques have been proposed as a way of achieving a v ery natural transition from informal requirements to a formal specific ation of the requirements. The paper presents a case study of a real-l ife system developed using such techniques. Both a top-level specifica tion and implementation semantics are given in temporal logic. In part icular, the progression from statements in English to temporal logic i s highlighted. A correctness proof that the implemented system satisfi es the specification has been produced.