Formal Verification of an Autonomous Grasping Algorithm
Marie Farrell, Nikos Mavrakis, Clare Dixon, Yang Gao · Rare & Special e-Zone (The Hong Kong University of Science and Technology) · 2020
Verifying that autonomous space robotic software behaves correctly is crucial, particularly since such software tends to be mission-critical, where a software failure often equates to mission failure. Formal verification is a technique used to reason about the correctness of a software system with the output providing a proof of correctness that the software behaves as it should. In this paper, we report on our use of the Dafny program verifier to formally verify a previously developed algorithm for grasping a spacecraft motor nozzle.