Stability Verification of a Control System using the Reachability Analysis

Humaira Salman, Farid Gul, Mian Ilyas Ahmad

Abstract


Model checking is a formal method technique used for the verification of safety critical and/or complex software and hardware systems. It provides accurate results by exhaustively exploring the abstract mathematical model of the system. This paper discusses the framework proposed for the verification of an underactuated inverted pendulum based two parallel wheeled vehicle. The physical model of the perceived system is designed for 2 DOF that is the pitch along x-axis and roll along y-axis. The mathematical model of the system is developed using the state-space approach and the system is analyzed using Matlab. Stability is introduced in to the system using a Linear Quadratic Regulator (LQR) with an Observer. This controlled system is analyzed and formally verified using the SpaceEx model checker. The stability verification of this system is performed using the reachability analysis. The model checker results shows the stability verification of the system over the convergence of infinite trajectories for a range of input values provided, showing advantage over simulation based techniques. The results also provide the phase portraits of the output variables in 2-D and 3-D planes.

Keywords


Linear Quadratic Regulator; Observer; Model Checking; Reachability; Exhaustive Search; Formal Method

Full Text:

PDF

References


G. R. Faulhaber. SEGWAY INC.

H. Gul, J. Ahmad, F. Gul, and M. Ilyas, "Modeling and formal verification of inverted pendulum based two-wheeled transportation vehicle," in SICE Annual Conference (SICE), 2012 Proceedings of, 2012, pp. 113-118.

F. Borrelli, "Constrained optimal control of linear and hybrid systems", 2003.

T. Wongpiromsarn, "Formal methods for design and verification of embedded control systems: Application to an autonomous vehicle", California Institute of Technology, 2010.

B. Mathieu, P. Melchior, A. Oustaloup, and C. Ceyral, "Fractional differentiation for edge detection," Signal Processing, vol. 83, pp. 2421-2432, 2003.

X. Moreau, C. Ramus-Serment, and A. Oustaloup, "Fractional differentiation in passive vibration control," Nonlinear Dynamics, vol. 29, pp. 343-362, 2002.

B. Vinagre, I. Petráš, I. Podlubny, and Y. Chen, "Using fractional order adjustment rules and fractional order reference models in model-reference adaptive control," Nonlinear Dynamics, vol. 29, pp. 269-279, 2002.

C. Baier and J. Katoen, "Principles of Model Checking (Representation and Mind Series). 2008," ed: The MIT Press.

B. Bérard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, et al., Systems and software verification: model-checking techniques and tools: Springer Publishing Company, Incorporated, 2010.

E. Asarin, T. Dang, and O. Maler, "The d/dt tool for verification of hybrid systems," in Computer Aided Verification, 2002, pp. 365-370.

G. Frehse, "An introduction to spaceex v0. 8," ed: December, 2010.

G. Frehse, C. Le Guernic, A. Donzé, S. Cotton, R. Ray, O. Lebeltel, et al., "SpaceEx: Scalable verification of hybrid systems," in Computer Aided Verification, 2011, pp. 379-395.

A. J. Van Der Schaft, J. M. Schumacher, A. J. van der Schaft, and A. J. van der Schaft, An introduction to hybrid dynamical systems vol. 251: Springer London, 2000.

(2010). SEGWAY ROBOTICS.

T. A. Henzinger, P.-H. Ho, and H. Wong-Toi, "HyTech: A model checker for hybrid systems," in Computer aided verification, 1997, pp. 460-463.

Steve’sLegway.

BALLBOT Project.

N. Baker, C. Brown, D. Dowling, J. Modra, and D. Tootell, "SON of EDGAR: State-space cONtrol of Electro-Drive Gravity-Aware Ride," Honours thesis, The University of Adelaide, 2006.

F. Grasser, A. D'Arrigo, S. Colombi, and A. C. Rufer, "JOE: a mobile, inverted pendulum," Industrial Electronics, IEEE Transactions on, vol. 49, pp. 107-114, 2002.

A.-Š. Vitko, Michal - Jurišica, Ladislav - Hubinský, Peter, "Data fusion and context awareness in autonomous robotics," International Journal of Mechanics and Control, vol. 5, pp. 29-39, 2004.

C.-H. Chiu, W.-R. Tsai, M.-H. Chou, and Y.-F. Peng, "Two-wheeled robot control based on self-tuning output recurrent CMAC," in Proceedings of the International MultiConference of Engineers and Computer Scientists 2009, 2009.

R. Grepl, "Balancing Wheeled Robot: Effective Modelling, Sensory Processing and Simplified Control," Engineering Mechanics, vol. 16, pp. 141-154, 2009.

S. Nawawi, M. Ahmad, and J. Osman, "Real-time control of a two-wheeled inverted pendulum mobile robot," World Academy of Science, Engineering and Technology, vol. 39, pp. 214-220, 2008.

A. Gmiterko, Vackova, x, and M., "Dynamic model of vehicle with two coaxial parallel wheels," in Applied Machine Intelligence and Informatics (SAMI), 2011 IEEE 9th International Symposium on, 2011, pp. 303-305.

K. M. Passino and N. Quijano, "Linear quadratic regulator and observer design for a flexible joint," Department of Electrical Engineering, The Ohio State University, 2002.

T. A. Henzinger, The theory of hybrid automata: Springer, 2000.

R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P.-H. Ho, X. Nicollin, et al., "The algorithmic analysis of hybrid systems," Theoretical computer science, vol. 138, pp. 3-34, 1995.

G. Frehse, "PHAVer: Algorithmic verification of hybrid systems past HyTech," in Hybrid Systems: Computation and Control, ed: Springer, 2005, pp. 258-273.


Refbacks

  • There are currently no refbacks.


Bookmark and Share


Creative Commons License
This work is licensed under a Creative Commons Attribution 3.0 License.