A safety-case approach for certifying adaptive systems

Adaptive systems—those that can change their behavior at runtime—pose new chal-lenges for certification, and particularly for traditional, standards-based methods of cer-tification such as DO-178B. These traditional methods are effective in conservative fields because they can establish a solid basis in experience and can incorporate the lessons learned from previous systems. They seem likely to prove less effective in fast-moving fields where innovation outstrips the pace at which experience can be incorporated into standards. Argument-based safety cases offer a plausible alternative basis for certification in these fast-moving fields. A safety case provides an explicit statement of safety claims, a body of evidence con-cerning 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 mod-eling 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 certifi-able 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. I