EAGER: Verification: The New Third Leg of Subsea Autonomous Systems Design

Iowa State University, Ames IA

Investigators

Abstract

Subsea Autonomous Systems, also called Autonomous Underwater Vehicles (AUVs) represent an important avenue for exploring and learning about our own planet, as well as others. They serve critical roles in studies of transportation, conservation, oceanography, marine biology, anthropology, and history, just to name a few. Autonomous subsea equipment has to be ultra-reliable to accomplish the given mission and avoid damaging or polluting the environment due to a system failure. They also must operate in harsh, dynamic, and unpredictable environments, more remote than space, and without the possibility of human intervention. This makes verification of AUVs extremely important. Currently, testing and analysis via ad hoc digital twins are the only standard AUV verification methods, but these fall short of the need for robust verification of AUVs. Formal methods provide proven tools and algorithms for both design-time and runtime verification of embedded systems, yet they are entirely unknown to AUV domain experts. AUV dynamic systems and control methods currently stand firmly on two legs: analysis and implementation. The project's impacts are adding a third leg of formal verification, laying the groundwork for real modernization and culture change in AUV verification education and industrial practice, and extending how formal methods are used for prognostics and digital twin technology. The project’s novelties are development and dissemination of design patterns and educational materials, based on new AUV-specific parameterized templates for formal verification, to increase the accessibility of formal methods to AUV domain experts. Since one of the biggest barriers to the adoption of formal methods in the AUV field is making formal methods tools intuitive, easy to use, and adaptable to AUV verification tasks, we contribute advances in these areas. We formulate AUV-based patterns for design-time formal verification and develop educational modules in AUV vocabulary. Since formal verification requires capturing system specifications in temporal logics, which is not an intuitive process for AUV engineers, we develop new, interactive, Graphical User Interface (GUI) representations of temporal logic specifications targeted to AUV engineers and refine them given feedback from AUV students. We also develop and release patterns for real-time (during the mission) AUV verification. To provide exciting yet practical educational experiences, we develop, teach, and release online laboratory education modules integrating this verification technology on-board real-life AUV hardware, complete with fault-injection and mitigation-triggering capabilities. Our hands-on labs using real AUVs will yield exciting yet practical experiences for AUV students and engineers (with trials at Rice University, Chevron, and Kongsberg), as well as supporting our efforts to inspire K-12 students to study engineering. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.