Resilience Talk 18 - Use of Assertion-based..Chris Harper, University of the West of England, UK

Validation of trustworthiness properties such as safety is difficult to achieve for autonomous systems, owing to the fact that those properties may need to be established over much larger and possibly even unbounded state spaces than has previously been necessary for manually controlled or basic automatic systems. While formal verification may be feasible of individual behavioural properties, it becomes impractical to co-verify multiple safety (or other) properties together in a manner that provides wide coverage of situated state spaces. Simulation testing and physical tests can exercise a complete system for all its properties together, a methodology we at Bristol Robotics Laboratory (BRL) refer to as “Corroborative V&V”. At BRL we have been investigating the use of simulation as a means to complement formal verification through the checking of assertions about the behaviour of autonomous systems, which can determine whether properties were violated during a given simulation run. We are developing a simulation testbench facility to perform these checks automatically in batch mode from an input test scenario. We review our development of a set of safety assertions for autonomous vehicle simulations derived from the UK Highway Code (UKHC), which we argue can provide evidence of safe driving behaviour in an autonomous vehicle.

Assertion-based validation by simulation could be used to evaluate post-facto resilience properties as well as preventative safety properties. There are few explicit rules in the UKHC regarding resilient behaviour, but it looks possible to develop assertion checks for resilience, and in this presentation we explore how this might be done.