Sound Development of Safety Supervisors
Mario Gleirscher, Lukas Plecher, Jan Peleska

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSafety Systems Engineering in Autonomy · Software Testing and Debugging Techniques · Formal Methods in Verification
