Farrell, Marie 
ORCID: 0000-0001-7708-3877, Mavrakis, Nikos, Ferrando, Angelo ORCID: 0000-0002-8711-4670, Dixon, Clare ORCID: 0000-0002-4610-9533 and Gao, Yang
(2022)
Formal Modelling and Runtime Verification of Autonomous Grasping for Active Debris Removal.
FRONTIERS IN ROBOTICS AND AI, 9.
639282-.
Abstract
Active debris removal in space has become a necessary activity to maintain and facilitate orbital operations. Current approaches tend to adopt autonomous robotic systems which are often furnished with a robotic arm to safely capture debris by identifying a suitable grasping point. These systems are controlled by mission-critical software, where a software failure can lead to mission failure which is difficult to recover from since the robotic systems are not easily accessible to humans. Therefore, verifying that these autonomous robotic systems function correctly is crucial. Formal verification methods enable us to analyse the software that is controlling these systems and to provide a proof of correctness that the software obeys its requirements. However, robotic systems tend not to be developed with verification in mind from the outset, which can often complicate the verification of the final algorithms and systems. In this paper, we describe the process that we used to verify a pre-existing system for autonomous grasping which is to be used for active debris removal in space. In particular, we formalise the requirements for this system using the Formal Requirements Elicitation Tool (FRET). We formally model specific software components of the system and formally verify that they adhere to their corresponding requirements using the Dafny program verifier. From the original FRET requirements, we synthesise runtime monitors using ROSMonitoring and show how these can provide runtime assurances for the system. We also describe our experimentation and analysis of the testbed and the associated simulation. We provide a detailed discussion of our approach and describe how the modularity of this particular autonomous system simplified the usually complex task of verifying a system post-development.
| Item Type: | Article |
|---|---|
| Uncontrolled Keywords: | autonomous grasping, formal verification, requirements elicitation, runtime verification, formal methods, active debris removal |
| Divisions: | Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science |
| Depositing User: | Symplectic Admin |
| Date Deposited: | 25 May 2022 13:38 |
| Last Modified: | 18 Jan 2023 21:01 |
| DOI: | 10.3389/frobt.2021.639282 |
| Open Access URL: | https://www.frontiersin.org/articles/10.3389/frobt... |
| Related URLs: | |
| URI: | https://livrepository.liverpool.ac.uk/id/eprint/3155486 |
Dimensions
Dimensions
