Runtime (Online) Verification of Autonomous Systems with Real-Time Reachability
Videos
10/25/2021
Several orders of magnitude progress made analyzing learning-enabled components (LECs) like neural networks and usage in autonomous CPS at design-time with NNV and other approaches (scalability, layer types, closed-loop interaction, etc.)
However, while improving confidence of such LECs before they are deployed is important, online monitoring at runtime is essential
How can we provide formal and provable guarantees of system-level behaviors, such as safety, online at runtime?
- Key idea: abstract LEC behaviors (see other approaches on out of distribution detection, etc.) and simply observe the influence of their behavior on plant/system-level at runtime
- Necessary technology: online reachability analysis of plant models, ideally with worst-case execution time (WCET) guarantees for implementation in embedded hardware
- Builds on real-time reachability of linear/nonlinear ordinary differential equations (ODEs) and hybrid automata with WCET guarantees, implemented as an anytime algorithm [FORTE’19, TECS’16, RTSS’14]
- Based on mixed face lifting reachability [Dang and Maler, HSCC’98 & HSCC’19 Test of Time Award Winner], using hyperrectangles (intervals) as state-space representation
[Tran et al, “Decentralized Real-Time Safety Verification for Distributed Cyber-Physical Systems”, FORTE’19]
[Johnson et al, “Real-Time Reachability for Verified Simplex Design”, TECS’16]
[Bak et al, “Real-Time Reachability for Verified Simplex Design”, RTSS’14]
http://www.verivital.com/rtreach/
The videos are presenting waypoint following scenarios, with and without thruster degradation and obstacle avoidance:
- Green curve: past trajectory
- Light-blue set: nominal control reachable set projected forward in time
- Red set: degraded control reachable set projected forward in time