A safety case provides an explicit statement of safety claims, a body of evidence concerning the system, and an argument, based on the evidence, that the system satisfies its claims; standards-based methods, in contrast, specify only the evidence to be produced.
A reasonable objection to safety cases is that many arguments---especially large, complex ones---can appear plausible, yet harbor flaws. There is a need for tools that can help analyze arguments. Some model-based design tools can do this, but generally operate at a far more detailed level of design than is appropriate for much of safety analysis. Some interactive theorem provers can do it, too, but they generally require notation and skills far removed from those found in aerospace and safety engineering.
In this paper we argue that analysis tools based on recent advances in formal methods (SMT solvers, infinite bounded model checkers, and k-induction) can provide suitable modeling notations, effective analysis, and push button automation. We illustrate the approach with a simple example based on a self-checking pair.
We further argue that monitors derived from a safety case provide a potentially certifiable means for entering an adaptive mode of behavior, and that monitors generated from a formally analyzed case can be "possibly perfect," which is a property that allows a novel kind of reliability analysis.
gzipped postscript, or plain postscript or PDF or crude ascii (for your Palm Pilot)