Title :
Temporal analysis of a microkernel
Author_Institution :
Dept. of Comput. Studies, Loughborough Univ. of Technol., UK
fDate :
1/1/1995 12:00:00 AM
Abstract :
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
Keywords :
formal specification; operating system kernels; program verification; temporal logic; case study; correctness proof; formal specification; implementation semantics; informal requirements; microkernel; real life system; temporal analysis; temporal logic techniques; top level specification;
Journal_Title :
Software Engineering Journal
