Trustworthy Systems

Formal system verification — extension, AOARD 114070

Authors

June Andronick, Gerwin Klein and Andrew Boyton

NICTA

UNSW

Abstract

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.

BibTeX Entry

  @techreport{Andronick_KB_12:tr,
    address          = {Sydney, Australia},
    author           = {Andronick, June and Klein, Gerwin and Boyton, Andrew},
    institution      = {NICTA},
    issn             = {1833-9646-5926},
    month            = may,
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/5926.pdf},
    title            = {Formal System Verification --- Extension, {AOARD} 114070},
    year             = {2012}
  }

Download