Multi-Platform, Multi-Architecture Runtime Verification for Autonomous Systems
System Health Management (SHM) is becoming critical to the deployment of a wide range of systems, including aircraft, spacecraft, satellites, and rovers. The most useful, important, and safety-critical jobs will require these systems to operate both intelligently and autonomously, with the ability to sense and respond to both nominal and off-nominal conditions. It is essential that we enable reasoning sufficient to detect critical failures on-board; as failure without warning may harm people, cause considerable property damage, or impact a fragile environment. We are challenged by the constraints of real-life embedded operation that limit the system instrumentation, space, timing, power, weight, cost, and other operating conditions of on-board, runtime SHM.
The Realizable, Responsive, Unobtrusive Unit (R2U2) analyzes specifications that combine temporal logics with probabilistic reasoning to provide formal assurances during runtime, enabling self-assessment of critical systems. Our goal is to enable intelligent autonomous operation through reliable diagnostics and prognostics while running aboard limited hardware and software, without affecting flight-certifiability. We highlight recent advances in SHM with R2U2, including adapting R2U2 for Robonaut2, whose leg joint arrived at ISU in January, 2018. We address challenges of realistic SHM specifications and look toward the future, asking the question, how do we proceed safely from here?