Because no single technique is adequate to cover a whole system in practice, a variety of complementing verification techniques will be needed to gain confidence in the correctness of robotic and autonomous systems [1]. In this talk I will concentrate on three aspects.
Coding: While much research has been invested into proving robotic navigation algorithms correct, little has been done to demonstrate that the implementations are bug-free. Coding in SPARK, an imperative, strongly-typed language used mainly in the safety-critical systems domain, enables formal proof to be used, with 97% of the proof obligations being discharged fully automatically and performance comparable to that of the original (buggy) implementations [2].
Designing: Being able to distinguish between design and implementation errors is critically important in practice. In the case of control systems, designs are typically written in Simulink before implementation in a programming language. On the example of stability, I will show how assertions can be used to capture the designer’s intent (i.e. the system requirements) in Simulink, and how simulation combined with automated formal proof can be used to gain confidence in the control system meeting these requirements [3].
Testing: The efficient generation of effective tests is essential for simulation-based testing [4]. In the context of a Human-Robot Interaction scenario, I will present our approach of exploiting the planning native to multi-agent systems to generate tests that achieve a high level of coverage as part of a coverage-driven verification method [5].
Finally, I will briefly outline the challenges of verifying robotic and autonomous systems, including specification, (more) automation, creatively combining techniques and, as addressed also by Arnaud Gotlieb, exploiting AI for verification. The work directly complements the contribution by Ana Cavalcanti on combining formal with simulation-based techniques, and the research presented by Arnaud Gotlieb and Rob Hierons on testing and model-based techniques.
[1] M. Webster, D. Western, D. Araiza-Illan, C. Dixon, K. Eder, M. Fisher and A. G. Pipe (2018). A Corroborative Approach to Verification and Validation of Human-Robot Teams. https://arxiv.org/abs/1608.07403
[2] P. Trojanek and K. Eder. Verification and testing of mobile robot navigation algorithms: A case study in SPARK. IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS).
pp. 1489-1494. Sep 2014. http://dx.doi.org/10.1109/IROS.2014.6942753
[3] D. Araiza Illan, K. Eder, A. Richards. Verification of Control Systems Implemented in Simulink with Assertion Checks and Theorem Proving: A Case Study. European Control Conference (ECC), pp. 2670 - 2675. Jul 2015. http://arxiv.org/abs/1505.05699 https://doi.org/10.1109/ECC.2015.7330941
[4] D. Araiza-Illan, D. Western, A. Pipe and K. Eder. Systematic and Realistic Testing in Simulation of Control Code for Robots in Collaborative Human-Robot Interactions. 17th Annual Conference Towards Autonomous Robotic Systems (TAROS 2016), pp. 20-32. Lecture Notes in Artificial Intelligence 9716. Springer, June 2016.
http://link.springer.com/chapter/10.1007/978-3-319-40379-3_3
[5] D. Araiza-Illan, A.G. Pipe, K. Eder. Intelligent Agent-Based Stimulation for Testing Robotic Software in Human-Robot Interactions. Proceedings of MORSE 2016, ACM, July 2016.
https://doi.org/10.1145/3022099.3022101
