Formal System Verification for Trustworthy Embedded Systems, Final Report AOARD 094160

Select |




Print


Andronick, June; Klein, Gerwin

Andronick, June; Klein, Gerwin


2011-04-19


Report


Sydney, Australia


This report summarises the work done in AOARD project 094160, Formal System Verification for Trustworthy Embedded Systems. We begin by revisiting the original motivation and work plan, which is of a verification framework that allows us to combine proofs from different levels of abstraction into one final, verifiable formal statement. We then present a high-level summary of the project outcomes: a fully formal, high-level architecture specification of a case study system; a formal behaviour specification of the main trusted component in the case study system; a high-level interleaving semantics for the execution of the whole system; and a formal security proof of the case study system, that examines all possible executions of the high-level system.


1833-9646-5614


nicta:5614


Andronick, June; Klein, Gerwin. Formal System Verification for Trustworthy Embedded Systems, Final Report AOARD 094160. 2011-04-19. nicta:5614.



Loading citation data...

Citation counts
(Requires subscription to view)