Verifying Pid Controller of Robot Car by Deltareachability Analysis

Verifying the safety of cyber-physical systems is widely recognized as an important concern, especially the safety of autonomous driving systems. In this paper, we focus on the PID controller of a robot car and verify its safety requirements. The verification of such systems is done through reachability analysis. However, this problem is undecidable. Therefore, we check the socalled delta-reachability, which is a weaker notion of reachability, to verify the safety requirements. We model the car as a hybrid system and utilize a delta-reachability solver for verification. Several combinations of PID gains are tested and evaluated.