Automatic Proving of Stability of the Cyber-Physical Systems in the Sense of Lyapunov with KeYmaera

摘要

The use of control systems in human life requires new methods to ensure the quality of embedded software at all levels of its production. In this work, we refer to the level of a cyber-physical system. These systems here can be specified using the hybrid automata abstraction to represent both discrete-time and continuous-time transitions, such models are known as hybrid models and they are expressed using the Differential dynamic logic. For the verification of continuous-state systems, a lot of simple models have been built around the KeYmaera tool as its tutorials in train, car and robotic domains. The advantage of the formal verification method over the simulation is the possibility to play with parameter values and check the requirements automatically without looking to resulting plots of system behavior over time. In this paper, we study how the hybrid theorem prover KeY-maera works while verifying control systems, in particular, using the Lyapunov method to prove stability of models encoded in a special notation of hybrid programs. We proceed to understand an example of a simple PD-controller and then move to a complex PID-controller model of a quadrotor stabilisation. We show that the process of such a verification can be carried out for rather complex systems initially taken in the form of engineering notation.