Formal Modelling and Runtime Verification of Autonomous Grasping for Active Debris Removal

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.

On-Orbit Robotic Grasping of a Spent Rocket Stage: Grasp Stability Analysis and Experimental Results

The increased complexity of the tasks that on-orbit robots have to undertake has led to an increased need for manipulation dexterity. Space robots can become more dexterous by adopting grasping and manipulation methodologies and algorithms from terrestrial robots. In this paper, we present a novel methodology for evaluating the stability of a robotic grasp that captures a piece of space debris, a spent rocket stage. We calculate the Intrinsic Stiffness Matrix of a 2-fingered grasp on the surface of an Apogee Kick Motor nozzle and create a stability metric that is a function of the local contact curvature, material properties, applied force, and target mass. We evaluate the efficacy of the stability metric in a simulation and two real robot experiments. The subject of all experiments is a chasing robot that needs to capture a target AKM and pull it back towards the chaser body. In the V-REP simulator, we evaluate four grasping points on three AKM models, over three pulling profiles, using three physics engines. We also use a real robotic testbed with the capability of emulating an approaching robot and a weightless AKM target to evaluate our method over 11 grasps and three pulling profiles. Finally, we perform a sensitivity analysis to demonstrate how a variation on the grasping parameters affects grasp stability. The results of all experiments suggest that the grasp can be stable under slow pulling profiles, with successful pulling for all targets. The presented work offers an alternative way of capturing orbital targets and a novel example of how terrestrial robotic grasping methodologies could be extended to orbital activities.