Towards a Verified Component Platform

Select |


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


Conference Material

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

November 03 - 06, 2013

Farmington, PA, USA


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.


New York


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.




Fernandez, M.; Kuz, I.; Klein, G.; Andronick, J. Towards a Verified Component Platform.[Conference Material]. New York: ACM; 2013-11. <a href="" target="_blank"></a>

Loading citation data...

Citation counts
(Requires subscription to view)