Rushby, J. (2009). A safety-case approach for certifying adaptive systems. In AIAA Infotech@ Aerospace Conference and AIAA Unmanned… Unlimited Conference (p. 1992).
Abstract
Adaptive systems- those that can change their behavior at runtime- pose new challenges for certification, and particularly for traditional, standards-based methods of certification 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 pervious 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 provide an explicit statement of safety claims, a body of evidence concerning they system, and an argument, based on the evidence, that the system satisfied its claims; standards-based methods, in contrast, specify only the evidence, that the system satisfies it’s 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 needs 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 formula analyzed case can be “possibly perfect,” which is a property that allows a novel kind of reliability analysis.