Trustworthy Systems

Towards a verified component platform


Matthew Fernandez, Ihor Kuz, Gerwin Klein and June Andronick




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

    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         = {},
    slides           = {},
    title            = {Towards a Verified Component Platform},
    year             = {2013}