Formal System Verification - Extension, AOARD 114070

Select |




Print


Andronick, June; Klein, Gerwin; Boyton, Andrew

Andronick, June; Klein, Gerwin; Boyton, Andrew


2012-05-17


Report


Sydney, Australia


The AOARD project FA2386-11-1-4070 aims at providing a provably correct initialiser of componentised systems. Taking as input a description of the desired components, including the desired authorised communication between them, the initialiser sets up the system and provides a proof that the resulting concrete machine state of the system matches the desired authority state. Within the scope of this project, we provide (1) a formal specification of the initialiser, in terms of the steps needed to create the components and their communication channels; and (2) a formal proof that this specification is correct in that it either fails safely or produces the desired state. The present document is an annual report of this project, presenting the status of the work undertaken so far. Namely, we have written the initialiser specification, we have set up a verification framework enabling modular reasoning and proofs, and we have progressed substantially on the proof.


1833-9646-5926


nicta:5926


Andronick, June; Klein, Gerwin; Boyton, Andrew. Formal System Verification - Extension, AOARD 114070. 2012-05-17. nicta:5926.



Loading citation data...

Citation counts
(Requires subscription to view)