Modular Verification of Autonomous Space Robotics



Farrell, Marie ORCID: 0000-0001-7708-3877, Cardoso, Rafael C ORCID: 0000-0001-6666-6954, Dennis, Louise A ORCID: 0000-0003-1426-1896, Dixon, Clare ORCID: 0000-0002-4610-9533, Fisher, Michael ORCID: 0000-0002-0875-3862, Kourtis, Georgios, Lisitsa, Alexei, Luckcuck, Matt ORCID: 0000-0002-6444-9312 and Webster, Matt ORCID: 0000-0002-8817-6881
Modular Verification of Autonomous Space Robotics. .

[img] Text
spaceconf.pdf - Submitted Version

Download (181kB) | Preview

Abstract

Ensuring that autonomous space robot control software behaves as it should is crucial, particularly as software failure in space often equates to mission failure and could potentially endanger nearby astronauts and costly equipment. To minimise mission failure caused by software errors, we can utilise a variety of tools and techniques to verify that the software behaves as intended. In particular, distinct nodes in a robotic system often require different verification techniques to ensure that they behave as expected. This paper introduces a method for integrating the various verification techniques that are applied to robotic software, via a First-Order Logic (FOL) specification that captures each node's assumptions and guarantees. These FOL specifications are then used to guide the verification of the individual nodes, be it by testing or the use of a formal method. We also outline a way of measuring our confidence in the verification of the entire system in terms of the verification techniques used.

Item Type: Conference or Workshop Item
Uncontrolled Keywords: cs.SE, cs.SE, cs.RO
Depositing User: Symplectic Admin
Date Deposited: 29 Aug 2019 09:53
Last Modified: 08 Nov 2019 11:00
Related URLs:
URI: http://livrepository.liverpool.ac.uk/id/eprint/3052772
Repository Staff Access