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

Area of Science:

• Space robotics and formal methods.
• Software verification and validation.
• Autonomous systems engineering.

Background:

• Active debris removal is essential for sustainable orbital operations.
• Autonomous robotic systems with grasping capabilities are key to debris capture.
• Software failures in space robotics can lead to mission failure due to inaccessibility.

Purpose of the Study:

• To formally verify a pre-existing autonomous grasping system for space debris removal.
• To ensure the reliability and correctness of mission-critical software controlling robotic systems.
• To demonstrate a practical approach to verifying post-development robotic software.

Main Methods:

• Formalizing system requirements using the Formal Requirements Elicitation Tool (FRET).
• Formally modeling software components and verifying them with the Dafny program verifier.
• Synthesizing runtime monitors using ROSMonitoring for runtime assurances.

Main Results:

• Successful formal verification of software components against formalized requirements.
• Demonstration of runtime monitors providing assurances for the autonomous grasping system.
• Analysis of experimental results from testbed and simulation environments.

Conclusions:

• Formal verification methods can be effectively applied to pre-existing space robotics systems.
• Modularity of the autonomous system simplified the verification process.
• The approach provides a pathway for enhancing the safety and reliability of space debris removal missions.