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.
