Composing Safe Systems
John Rushby
Invited paper presented at the
8th International Symposium on Formal Aspects of Component Software
(FACS'11), Oslo, Norway, September 14-16, 2011.
To appear in post-proceedings
(Springer LNCS).
Abstract
Failures in component-based systems are generally due to unintended or
incorrect interactions among the components. For safety-critical
systems, we may attempt to eliminate unintended interactions, and to
verify correctness of those that are intended. We describe the value
of partitioning in eliminating unintended interactions, and of
assumption synthesis in developing a robust foundation for
verification. We show how model checking of very abstract designs
can provide mechanized assistance in human-guided assumption
synthesis.
PDF
Slides
PDF
BibTeX Entry
TBD (LNCS volume not yet available).
Having trouble reading our papers?
Return to John Rushby's bibliography page
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page