Verification of autonomous systems using embedded behavior auditors
Daniel L. Dvorak, E. A. Tailor · AIP conference proceedings · 1999
The prospect of highly autonomous spacecraft and rovers is exciting for what they can do with onboard decision making, but also troubling for what they might do [improperly] without human-in-the-loop oversight. The single biggest obstacle to acceptance of highly autonomous software control systems is doubt about their trustworthiness as a replacement for human analysis and decision-making. Such doubts can be addressed with a comprehensive system verification effort, but techniques suitable for conventional sequencer-based systems are inadequate for reactive systems. This paper highlights some of the key features that distinguish autonomous systems from their predecessors and then focuses on one approach to aid in their verification using a “lightweight” formal method. Specifically, we present a little language that enables system engineers and designers to specify expected behavior in the form of invariants, state machines, episodes, and resource constraints, and a way of compiling such specifications and linking them into the operational code as embedded behavior auditors. Such auditors become part of the overall fault-detection design, checking system behavior in real-time, not only in the test-bed but also in flight.