University of SaskatchewanHARVEST
  • Login
  • Submit Your Work
  • About
    • About HARVEST
    • Guidelines
    • Browse
      • All of HARVEST
      • Communities & Collections
      • By Issue Date
      • Authors
      • Titles
      • Subjects
      • This Collection
      • By Issue Date
      • Authors
      • Titles
      • Subjects
    • My Account
      • Login
      JavaScript is disabled for your browser. Some features of this site may not work without it.
      View Item 
      • HARVEST
      • Electronic Theses and Dissertations
      • Graduate Theses and Dissertations
      • View Item
      • HARVEST
      • Electronic Theses and Dissertations
      • Graduate Theses and Dissertations
      • View Item

      Formal verification of a real-time operating system

      Thumbnail
      View/Open
      TELLEZ-ESPINOSA-THESIS.pdf (1002.Kb)
      Date
      2012-08-30
      Author
      Tellez Espinosa, Gadi de Leon
      Type
      Thesis
      Degree Level
      Masters
      Metadata
      Show full item record
      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.
      Degree
      Master of Science (M.Sc.)
      Department
      Computer Science
      Program
      Computer Science
      Supervisor
      Dutchyn, Christopher
      Committee
      Bolton, Ronald; Horsch, Michael; Makaroff, Dwight
      Copyright Date
      August 2012
      URI
      http://hdl.handle.net/10388/ETD-2012-08-565
      Subject
      Formal Verification
      FreeRTOS
      Real-Time Operating System
      Separation Logic
      Coq
      Compcert
      Collections
      • Graduate Theses and Dissertations
      University of Saskatchewan

      University Library

      © University of Saskatchewan
      Contact Us | Disclaimer | Privacy