A Safety-Case Approach For Certifying Adaptive Systems

John Rushby

AIAA Infotech@Aerospace Conference, Seattle WA, April 2009

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

Code

SAL specification for the example

Slides

gzipped postscript, or plain postscript or PDF or crude ascii (for your Palm Pilot)

BibTeX Entry

           TBD
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