Finite State-Machine Verification Applied to Hybrid Systems 2012-36-0429

Hybrid systems are characterized by a composition of discrete and continuous dynamics. In particular, the system has a continuous evolution and occasional jumps. The jumps are caused either by controllable, uncontrollable external events or by its continuous evolution. Inevitably, this type of system is present in mobility devices such as cars, ships, and aircrafts. Efforts to develop this type of system have increasingly suffered from cost and schedule overruns. In fact, the verification of such systems has become a key activity in the development life cycle. Historically, such activity demands experts and high efforts, and uses ad-hoc methods. Therefore, the aim of this work is to apply finite state-machine verification to hybrid systems. To do that, a small part of the vast theory of automatic test suite generation for this type of discrete behavior and system is applied in a model-based testing approach, showing an effective and reproducible alternative for automatic test suite generation. A case study considering the problem of the inverted pendulum was developed to evaluate the suggested approach. The inverted pendulum is a model of the attitude control for satellite launch vehicles at its departure. The uniqueness of an inverted pendulum, due to its natural instability, provides various researches in areas of systems, control, electronics and software. Furthermore, the inverted pendulum is a classic hybrid system, since it is composed of continuous dynamics (stabilization of the pendulum in a vertical axis) and discrete logics (mode management). The results obtained so far with this case study have given strong indications that the approach can bring significant gains for the effectiveness of verification coupled with the reduction of time for planning and execution of verification, as well as contributing to fulfill certification requirements.