Towards a Verified Component Platform

Select |




Print


Fernandez, M.; Kuz, I.; Klein, G.; Andronick, J.


2013-11


Conference Material


PLOS '13 Proceedings of the Seventh Workshop on Programming Languages and Operating Systems


November 03 - 06, 2013


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.


ACM


New York


Data61


https://doi.org/10.1145/2525528.2525535


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.


English


9781450324601


nicta:7281


Fernandez, M.; Kuz, I.; Klein, G.; Andronick, J. Towards a Verified Component Platform. In: PLOS '13 Proceedings of the Seventh Workshop on Programming Languages and Operating Systems ; November 03 - 06, 2013; Farmington, PA, USA. New York: ACM; 2013-11. 1-7. https://doi.org/10.1145/2525528.2525535



Loading citation data...

Citation counts
(Requires subscription to view)