Modeling and Formal Verification, Using Model Checking, of an Inverted Pendulum Based, Coaxially Parallel, TwoWheeled Transportation Vehicle

Abstract

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 automated control systems. But in the very near few years, some model checking tools have been developed for control systems verification. This research includes the modeling of a controlled system and proposes the formal verification of the stability of a 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 statespace 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 checking tool. SpaceEx model checker is used for the formal analysis of this system to analyze and verify the designed system. The analysis and verification is done by applying the reachability analysis. Our results also show that the system's infinite trajectories convergence for a range of initial values is also a huge advantage over simulation based analysis.