Towards a Verified Component Platform

Select |




Print


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

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


2013-11-03


Conference Material


Programming Languages and Operating Systems (PLOS)


Farmington, PA, USA


1-7


This paper describes ongoing work on a new technique for reducing the cost of assurance of large software systems by building on a verified component platform. From a component architecture description, we automatically derive a formal model of the system and a semantics for the runtime behaviour of generated inter-component communication code. We can prove wellformedness properties of the architecture automatically and provide a framework in which users can reason about their component code and its behaviour. By leveraging the isolation properties and communication guarantees of a formally verified platform, correctness arguments for critical components can be derived independently and composed together to reason about system-level correctness.


http://www.plosworkshop.org/2013/


This material is based on research sponsored by Air Force Research Laboratory and the Defense Advanced Research Projects Agency (DARPA) under agreement number FA8750-12-9-0179. The U.S. Government is authorized to reproduce and distribute reprints for Governmental purposes notwithstanding any copyright notation thereon. The views and conclusions contained herein are those of the authors and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of Air Force Research Laboratory, the Defense Advanced Research Projects Agency or the U.S. Government.


nicta:7281


Fernandez, Matthew; Kuz, Ihor; Klein, Gerwin; Andronick, June. Towards a Verified Component Platform. In: Programming Languages and Operating Systems (PLOS); Farmington, PA, USA. 2013-11-03. 1-7.



Loading citation data...

Citation counts
(Requires subscription to view)