StatDev: Safety Verification of Autonomous Systems Under Timing Uncertainties
Quantitative Safety
Imagine a scenario, where a robot, is trying to reach its destination, avoiding obstacles.
The obstacles are given in purple.
And the destination is marked with a flag.
The planned path of the robot, to its destination, is given in black. This we call the nominal trajectory.
Running Multiple Jobs Together
Path Follower Missing Deadline
What Does StatDev Do?
StatDev: Safety Verification Under Timing Uncertainties
A tool that can compute the maximum deviation from the nominal behavior under deadline misses.
The code is available open source through a public GitHub repository.
Questions? Email Bineet Ghosh at bineet@cs.unc.edu
More Details?
The tool is based on the following work: Statistical Hypothesis Testing of Controller Implementations Under Timing Uncertainties by Bineet Ghosh et al. In: The 28th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA). 2022. (To appear). Best Paper Candidate.
Verifying such quantitative safety properties involves performing a reachability analysis that is computationally intractable, or is too conservative. To alleviate these problems we propose to provide statistical guarantees over behavior of control systems with timing uncertainties. More specifically, we present a Bayesian hypothesis testing method based on Jeffreys’s Bayes factor test that estimates deviations from a nominal or ideal behavior. We show that our analysis can provide, with high confidence, tighter estimates of the deviation from nominal behavior than using known reachability based methods.