Sound Development of Safety Supervisors

TL;DR

This paper proposes a rigorous, tool-supported workflow combining verified synthesis and testing for the sound development of safety supervisors in autonomous systems, exemplified with collaborative robotics.

Contribution

It introduces a novel workflow integrating formal verified synthesis with complete testing to enhance safety supervisor development.

Findings

Workflow is sound and rigorously validated.

Applicable to modern autonomous systems.

Demonstrated with a collaborative robotics example.

Abstract

Safety supervisors are controllers enforcing safety properties by keeping a system in (or returning it to) a safe state. The development of such high-integrity components can benefit from a rigorous workflow integrating formal design and verification. In this paper, we present a workflow for the sound development of safety supervisors combining the best of two worlds, verified synthesis and complete testing. Synthesis allows one to focus on problem specification and model validation. Testing compensates for the crossing of abstraction, formalism, and tool boundaries and is a key element to obtain certification credit before entry into service. We establish soundness of our workflow through a rigorous argument. Our approach is tool-supported, aims at modern autonomous systems, and is illustrated with a collaborative robotics example.