Successful Swarms: Operator Situational Awareness with Modelling and Verification at Runtime

Robot swarms, through redundancy, offer faulttolerant distributed sensing and actuation, but can lack complex mission-level decision making. Pairing a human operator with the swarm can improve decision making but only if the operator maintains situational awareness-knowledge of the current state of the swarm-as well as being able to anticipate future states. We show how formal methods, in the form of probabilistic models, executed and verified at runtime alongside the system can aid situational awareness by providing valuable insight into both current and future situations. Two models, for determining task and mission success probabilities, are given, and we show that statistical model checking allows timely approximate predictions that take no more than 1s while staying within 2% of the exact solution. We highlight and implement approaches to display this information to an operator, and show how models can be used to try what-if scenarios before decisions are made.