Title: Verifying Behaviour of Swarms of Autonomous Cyber Physical Systems

Author(s): Colin O’Halloran, Nick Tudor, William Simmonds

Publication Event: Proceedings of the Twenty-seventh Safety-Critical Systems Symposium, Bristol, UK

Publication Date: 2019-02-06

Resource URL: https://scsc.uk/r1072.pdf

Abstract:

An autonomous vehicle individually has to comply with its behavioural specification. The specification of the autonomy requirements must: be understandable; verify the absence of undesired behaviour and be able to verify what happens when something goes wrong. A swarm comprising a collection of autonomous vehicles has to comply with the behavioural specification for the swarm. Such a specification will cover the task that the swarm needs to achieve and coherence of the swarm. We discuss the results of two IUK funded projects on verifying large swarm behaviours of simple robots and small swarms of autonomous sea vessels whose software designs are represented in Simulink® / Stateflow®. A compositional approach was taken to first verifying the designs of individual autonomous systems and then verifying the swarm properties of the composed specifications.