Trustworthy Systems

Towards a verified component platform

Authors

Matthew Fernandez, Ihor Kuz, Gerwin Klein and June Andronick

NICTA\ UNSW

Abstract

This paper describes ongoing work on a new technique for reducing the cost of assurance of large software systems by building on a verified component platform. From a component architecture description, we automatically derive a formal model of the system and a semantics for the runtime behaviour of generated inter-component communication code. We can prove wellformedness properties of the architecture automatically and provide a framework in which users can reason about their component code and its behaviour. By leveraging the isolation properties and communication guarantees of a formally verified platform, correctness arguments for critical components can be derived independently and composed together to reason about system-level correctness.

BibTeX Entry

  @inproceedings{Fernandez_KKA_13,
    address          = {Farmington, PA, USA},
    author           = {Fernandez, Matthew and Kuz, Ihor and Klein, Gerwin and Andronick, June},
    booktitle        = {Workshop on Programming Languages and Operating Systems (PLOS)},
    month            = nov,
    pages            = {1--7},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/7281.pdf},
    slides           = {https://trustworthy.systems/publications/nicta_slides/7281.pdf},
    title            = {Towards a Verified Component Platform},
    year             = {2013}
  }

Download