Complete Test of Synthesised Safety Supervisors for Robots and Autonomous Systems
Open Access
- 21 October 2021
- journal article
- Published by Open Publishing Association in Electronic Proceedings in Theoretical Computer Science
- Vol. 348, 101-109
- https://doi.org/10.4204/eptcs.348.7
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.This publication has 24 references indexed in Scilit:
- Complete model-based equivalence class testing for nondeterministic systemsFormal Aspects of Computing, 2017
- Checking Experiments for Symbolic Input/Output Finite State MachinesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2016
- Complete model-based equivalence class testingInternational Journal on Software Tools for Technology Transfer, 2014
- Model-based testing of software and systems: recent advances and challengesInternational Journal on Software Tools for Technology Transfer, 2012
- PRISM 4.0: Verification of Probabilistic Real-Time SystemsLecture Notes in Computer Science, 2011
- A Logical Basis for Component-Oriented Software and Systems EngineeringThe Computer Journal, 2010
- Stochastic Model CheckingPublished by Springer Science and Business Media LLC ,2007
- An Improved Conformance Testing MethodLecture Notes in Computer Science, 2005
- A Tutorial on UppaalLecture Notes in Computer Science, 2004
- Negative scenarios for implied scenario elicitationACM SIGSOFT Software Engineering Notes, 2002