Skip to main content
CSIRO Logo Data 61 logo

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,
    author           = {Fernandez, Matthew and Kuz, Ihor and Klein, Gerwin and Andronick, June},
    month            = nov,
    year             = {2013},
    title            = {Towards a Verified Component Platform},
    address          = {Farmington, PA, USA},
    pages            = {1--7},
    booktitle        = {Workshop on Programming Languages and Operating Systems (PLOS)},
    paperurl         = {https://ts.data61.csiro.au/publications/nicta_full_text/7281.pdf},
    slides           = {/publications/nicta_slides/7281.pdf}
  }

Download