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).


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.




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