View Item 
        •   Utrecht University Student Theses Repository Home
        • UU Theses Repository
        • Theses
        • View Item
        •   Utrecht University Student Theses Repository Home
        • UU Theses Repository
        • Theses
        • View Item
        JavaScript is disabled for your browser. Some features of this site may not work without it.

        Browse

        All of UU Student Theses RepositoryBy Issue DateAuthorsTitlesSubjectsThis CollectionBy Issue DateAuthorsTitlesSubjects

        Compiling an Haskell EDSL to C: A new C back-end for the Copilot runtime verification framework

        Thumbnail
        View/Open
        3705269.pdf (1.642Mb)
        Publication date
        2018
        Author
        Dedden, F.H.
        Metadata
        Show full item record
        Summary
        Electronics and computers are all around us, ranging from cellphones to aircraft avionics. Some systems, including aircraft and nuclear powerplants, are considered safety-critical: failure can lead to the injury or death of humans. These ultra-critical systems require a very small probability of failure (<10^-9), and are strictly certified by regulatory bodies. Static software verification can aid in improving the safety of these systems, but only scales for a limited number of properties. Functional verification often requires the use of interactive theorem provers and are not practical for industrial scale systems. There is also a push to apply highly nondeterministic techniques such as machine learning in safety-critical systems, which cannot be verified using traditional proof techniques. Runtime verification, where specifications are checked during execution can allow us to verify software systems that cannot be verified by other means. The Haskell based Copilot runtime verification framework has been developed as part of a NASA project applying runtime verification to real-time embedded C programs. A lack of first class support for arrays and structs limited Copilot's practical usability. By replacing the current Atom and SBV-based code generation back-ends by a new, custom designed one, we are able to implement both arrays and structs as first class members of our specification. Both C structs and arrays are not straightforward to represent in Haskell, and require special attention. In particular type literals have been used to implement a safer array than Haskell normally allows. Having native support for structs and arrays simplifies monitor specifications, and makes writing them easier and quicker. In addition, a tailored code generator also allows us to improve on the readability of the generated output code, making debugging and tracing easier, which in the end aids in making systems safer.
        URI
        https://studenttheses.uu.nl/handle/20.500.12932/29176
        Collections
        • Theses
        Utrecht university logo