Verifying a PI Controller using SoapBox and Stabhyli
Eike Möhlmann, Willem Hagemann, Astrid Rakow · EPiC series in computing · 2018
We describe practical experiences on verifying a steering controller specification. The hybrid automaton implements a PI control rule and considers the vehicle's velocity as input from the environment. By combining the tools Stabhyli and SoapBox, we establish several safety and liveness properties for the steering controller, including convergence towards an equilibrium.