R2U2: Runtime Verification Takes Off! (Keynote)

Runtime Verification (RV) has become critical to the deployment of intelligent, autonomous systems, including aircraft, spacecraft, satellites, rovers, and robots. The most useful, important, and safety-critical jobs require these systems to reliably sense and respond to both nominal and off-nominal conditions. They must react to challenging environments, and detect critical failures on-board, in real time to enable mitigation triggering. 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 verification. While the research area of RV is vast, there is a dearth of RV tools that can operate within these constraints, and without violating, e.g., FAA rules for flight certification. The Realizable, Responsive, Unobtrusive Unit (R2U2) uniquely fills this need, analyzing formal system requirements on-board flight systems during runtime. We overview how R2U2 works and highlight recent success stories, including embedding on-board various UAS, a sounding rocket, the humanoid robot Robonaut2, and NASA's Lunar Gateway.