Modeling and formal verification of inverted pendulum based two-wheeled transportation vehicle

Formal methods have been used to verify the correctness and stability of hardware and software systems for the last few decades. It has numerous applications in system´s analysis, safety and detection of subtle bugs and errors. The approach utilizes certain mathematical properties, methods and axioms to exhaustively explore all the states of the system. It gives precise and better results than simulation and numerical methods based analysis and verification, since the later techniques cannot give exhaustive results and could suffer from discretization and round-off errors. Model checking is an important formal method that verifies systems by exhaustively exploring the system´s abstract mathematical model using smart domain-specific abstraction techniques. For certain reasons, model checking has not been previously used for the verification of control systems. But in the very near few years, some model checking tools have also been developed for control systems verification. This paper includes the verification of a controlled system and proposes the formal verification of the stability of coaxially parallel two-wheeled transportation vehicle. The control system model perceived is a dynamic, inverted pendulum based, coaxially parallel two-wheeled human transportation vehicle. The dynamic physical model of the system is simplified and designed for 2-D motion that is the pitch control and the linear forward/backward motion. A mathematical model is then developed from this dynamic physical model of the system, using the state-space approach. Then, a linear quadratic regulator (LQR) with an observer is designed to stabilize this system. Later, the system is formally verified for stability using the model checker SpaceEx.