Static Verification of Spacecraft Procedures
Erin Connors, Cesar A. Munoz, Cameron Schnur, Radu I. Siminiceanu · AIAA Infotech@Aerospace Conference · 2009
The Automation for Operations project (A4O), which is part of NASA’s Exploration Technology Development Program, aims at advancing automation technology in support of spacecraft operations. Procedures that encode the means by which spacecraft systems are operated are a critical target of automation technology. In this paper, we present a static verification tool for NASA’s Procedure Representation Language (PRL), a XMLbased notation for specifying manual and autonomous operation procedures. The tool checks PRL files for valid syntactical structure and semantics, ensures that procedures are invoked correctly, consults a system-representation database to validate usage constraints, and, finally, verifies the consistency of logical conditions using a constraint solver. All these checks are implemented statically, i.e., at the moment when procedures are being created, before they are deployed and executed. The tool has been fully integrated into the Procedure Integrated Development Environment (PRIDE), a PRL authoring and editor environment developed by NASA.