Trustworthy Systems

Formalisation of a component platform

Authors

Matthew Fernandez, Ihor Kuz and Gerwin Klein

NICTA

UNSW

Published:

Poster presented at Operating Systems Design and Implementation 2012

Abstract

Developing and maintaining large safety- and security-critical software systems can be complex and error prone when based on a monolithic design. Techniques like formal verification can be used to gain a measure of confidence in the correctness of the system, but applying these to code bases at a scale of millions of lines of code remains infeasible. Using component-based development to design a system from composable elements has the potential to lower the costs of both development and formal reasoning about the properties of the system. While there have been attempts in the past to apply formal methods to component systems, existing work assumes the correctness of the component platform itself. This poster reports on ongoing work on the formal modelling and verification of a component platform for systems' development.

BibTeX Entry

  @misc{Fernandez_KK_12_2,
    address          = {Hollywood, CA, USA},
    author           = {Fernandez, Matthew and Kuz, Ihor and Klein, Gerwin},
    howpublished     = {Poster presented at Operating Systems Design and Implementation 2012},
    keywords         = {camkes, sel4},
    month            = oct,
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/6337.pdf},
    title            = {Formalisation of a Component Platform},
    year             = {2012}
  }

Download