Automated Verification of a Component Platform

Select |




Print


Fernandez, Matthew; Andronick, June; Klein, Gerwin; Kuz, Ihor

Fernandez, Matthew; Andronick, June; Klein, Gerwin; Kuz, Ihor


2015-08-01


Report


Sydney, Australia


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.


camkes, sel4, autocorres


1833-9646-9034


nicta:9034


Fernandez, Matthew; Andronick, June; Klein, Gerwin; Kuz, Ihor. Automated Verification of a Component Platform. 2015-08-01. nicta:9034.



Loading citation data...

Citation counts
(Requires subscription to view)