Repository logo

Formal verification of a real-time operating system

dc.contributor.advisorDutchyn, Christopheren_US
dc.contributor.committeeMemberBolton, Ronalden_US
dc.contributor.committeeMemberHorsch, Michaelen_US
dc.contributor.committeeMemberMakaroff, Dwighten_US
dc.creatorTellez Espinosa, Gadi de Leonen_US 2012en_US
dc.description.abstractErrors caused by the interaction of computer systems with the physical world are hard to mitigate but errors related to the underlying software can be prevented by a more rigorous development of software code. In the context of critical systems, a failure caused by software errors could lead to consequences that are determined to be unacceptable. At the heart of a critical system, a real-time operating system is commonly found. Since the reliability of the entire system depends upon having a reliable operating system, verifying that the operating systems functions as desired is of prime interest. One solution to verify the correctness of significant properties of an existing real-time operating system microkernel (FreeRTOS) applies assisted proof checking to its formalized specification description. The experiment consists of describing real-time operating system characteristics, such as memory safety and scheduler determinism, in Separation Logic — a formal language that allows reasoning about the behaviour of the system in terms of preconditions and postconditions. Once the desired properties are defined in a formal language, a theorem can be constructed to describe the validity of such formula for the given FreeRTOS implementation. Then, by using the Coq proof assistant, a machine-checked proof that such properties hold for FreeRTOS can be carried out. By expressing safety and deterministic properties of an existing real-time operating systems and proving them correct we demonstrate that the current state-of-the-art in theorem-based formal verification, including appropriate logics and proof assistants, make it possible to provide a machine-checked proof of the specification of significant properties for FreeRTOS.en_US
dc.subjectFormal Verificationen_US
dc.subjectReal-Time Operating Systemen_US
dc.subjectSeparation Logicen_US
dc.titleFormal verification of a real-time operating systemen_US
dc.type.materialtexten_US Scienceen_US Scienceen_US of Saskatchewanen_US of Science (M.Sc.)en_US


Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
1002.92 KB
Adobe Portable Document Format
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
1021 B
Plain Text