Automated verification of a component platform
Authors
NICTA
UNSW
Abstract
This document outlines various criteria defining the correctness of a component platform, and describes a process for automatic verification of some of these criteria for the CAmkES component platform. Generated proofs are provided for a sample system as an example of the output artefacts and their relationship to both hand written formal reasoning and generated code. Our correctness properties depend upon an interactive theorem prover and some straightforward translation tools. We consider our assumptions and resulting trusted computing base to be acceptable in a high assurance software environment.
This report is an extension to previous reports on the formalisation of the CAmkES component platform and a familiarity with these previous documents is assumed.
BibTeX Entry
@techreport{Fernandez_AKK_15:tr, address = {Sydney, Australia}, author = {Fernandez, Matthew and Andronick, June and Klein, Gerwin and Kuz, Ihor}, institution = {NICTA and UNSW}, issn = {1833-9646-9034}, keywords = {camkes, sel4, autocorres}, month = aug, paperurl = {https://trustworthy.systems/publications/nicta_full_text/9034.pdf}, title = {Automated Verification of a Component Platform}, year = {2015} }