Formal verification of a real-time operating system
| dc.contributor.advisor | Dutchyn, Christopher | en_US |
| dc.contributor.committeeMember | Bolton, Ronald | en_US |
| dc.contributor.committeeMember | Horsch, Michael | en_US |
| dc.contributor.committeeMember | Makaroff, Dwight | en_US |
| dc.creator | Tellez Espinosa, Gadi de Leon | en_US |
| dc.date.accessioned | 2013-01-03T22:32:12Z | |
| dc.date.available | 2013-01-03T22:32:12Z | |
| dc.date.created | 2012-08 | en_US |
| dc.date.issued | 2012-08-30 | en_US |
| dc.date.submitted | August 2012 | en_US |
| dc.description.abstract | Errors 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.identifier.uri | http://hdl.handle.net/10388/ETD-2012-08-565 | en_US |
| dc.language.iso | eng | en_US |
| dc.subject | Formal Verification | en_US |
| dc.subject | FreeRTOS | en_US |
| dc.subject | Real-Time Operating System | en_US |
| dc.subject | Separation Logic | en_US |
| dc.subject | Coq | en_US |
| dc.subject | Compcert | en_US |
| dc.title | Formal verification of a real-time operating system | en_US |
| dc.type.genre | Thesis | en_US |
| dc.type.material | text | en_US |
| thesis.degree.department | Computer Science | en_US |
| thesis.degree.discipline | Computer Science | en_US |
| thesis.degree.grantor | University of Saskatchewan | en_US |
| thesis.degree.level | Masters | en_US |
| thesis.degree.name | Master of Science (M.Sc.) | en_US |