Project

General

Profile

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

 

Files

degraded-waypoint-following-4x.mp4 (2.77 MB) degraded-waypoint-following-4x.mp4 Degradation scenario without obstacles Daniel Stojcsics, 10/25/2021 08:50 AM
degraded-obstacle-avoidance4x.mp4 (5.14 MB) degraded-obstacle-avoidance4x.mp4 Degradation scenario with obstacle avoidance Daniel Stojcsics, 10/25/2021 08:50 AM
way-point-following-obstacle-avoidance_4x.mp4 (6.19 MB) way-point-following-obstacle-avoidance_4x.mp4 Nominal scenario with obstacle avoidance Daniel Stojcsics, 10/25/2021 08:50 AM
waypoint_following_normal.mp4 (76.9 MB) waypoint_following_normal.mp4 Nominal scenario without obstacles Daniel Stojcsics, 10/25/2021 08:51 AM