Complete Test of Synthesised Safety Supervisors for Robots and Autonomous Systems

TL;DR

This paper proposes a comprehensive testing approach for synthesised safety supervisors in robots and autonomous systems, ensuring their correctness and safety properties through abstract testing and observational equivalence verification.

Contribution

It introduces a method to generate complete test suites from abstract models to verify the correctness of safety supervisor code in autonomous systems.

Findings

Complete test suite generation from abstract models

Verification of observational equivalence between abstract and concrete controllers

Enhanced assurance of safety supervisor correctness

Abstract

Verified controller synthesis uses world models that comprise all potential behaviours of humans, robots, further equipment, and the controller to be synthesised. A world model enables quantitative risk assessment, for example, by stochastic model checking. Such a model describes a range of controller behaviours some of which -- when implemented correctly -- guarantee that the overall risk in the actual world is acceptable, provided that the stochastic assumptions have been made to the safe side. Synthesis then selects an acceptable-risk controller behaviour. However, because of crossing abstraction, formalism, and tool boundaries, verified synthesis for robots and autonomous systems has to be accompanied by rigorous testing. In general, standards and regulations for safety-critical systems require testing as a key element to obtain certification credit before entry into service. This work-in-progress paper presents an approach to the complete testing of synthesised supervisory controllers that enforce safety properties in domains such as human-robot collaboration and autonomous driving. Controller code is generated from the selected controller behaviour. The code generator, however, is hard, if not infeasible, to verify in a formal and comprehensive way. Instead, utilising testing, an abstract test reference is generated, a symbolic finite state machine with simpler semantics than code semantics. From this reference, a complete test suite is derived and applied to demonstrate the observational equivalence between the synthesised abstract test reference and the generated concrete controller code running on a control system platform.