This content is not included in
your SAE MOBILUS subscription, or you are not logged in.
Finite State-Machine Verification Applied to Hybrid Systems
Technical Paper
2012-36-0429
ISSN: 0148-7191, e-ISSN: 2688-3627
Annotation ability available
Sector:
Language:
English
Abstract
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.
Authors
Topic
Citation
Romero, A., Ambrosio, A., and Souza, M., "Finite State-Machine Verification Applied to Hybrid Systems," SAE Technical Paper 2012-36-0429, 2012, https://doi.org/10.4271/2012-36-0429.Also In
References
- Bender, K. Broy, M. Peter, I. Pretschner, A. Stauner, T. 2002 Model based development of hybrid systems Modelling, Analysis, and Design of Hybrid Systems, volume 279 of Lecture Notes on Control and Information Sciences 37 52 Springer Verlag July 2002
- Brillout, A He, N. Mazzucchi, M Kroening, D. Purandare, M. Rümmer, P. Weissenbacher, G. 2010 Mutation-Based Test Case Generation for Simulink Models Formal Methods for Components and Objects Lecture Notes in Computer Science 2010 6286 2010 208 227 10.1007/978-3-642-17071-3_11
- CEA 2012 Papyrus site http://papyrusuml.org 23 April 2012
- Cristiá, M. Santiago, V. Vijaykumar, N.L. 2010 On Comparing and Complementing two MBT approaches Vargas, Fabián Cota, Erika LATW, IEEE Computer Society 1 6
- Gadkari, A. Yeolekar, A. Suresh, J. Ramesh, S. Mohalik, S. Shashidar, K.C. 2008 AutoMOTGen: Automatic model oriented test generator for embedded control systems Gupta, A. Malik, S. Computer Aided Verication (CAV) 5123 2008 Springer 2008 204 208
- Gromov, M. Popov, D. Yevtushenko, N. 2008 Deriving test suites for timed Finite State Machines Proceedings of IEEE East-West Design & Test Symposium 08 Kharkov SPD FL Stepanov V.V. 2008 339 343
- Hopcroft, J. Ullman, J. 1979 Introduction to automata theory, languages, and computation Addison-Wesley Publishing company
- Jia, Y. Harman, M. 2010 An analysis and survey of the development of mutation testing IEEE Transactions on Software Engineering (TSE)
- JPLAVIS 2012 PLAVIS - Platform for Software Validation & Integration on Space Systems http://www.icmc.usp.br/∼arineiza 03 May 2012
- Object Management Group (OMG) 2010a Systems Modeling Language SysML: Version 1.2 USA OMG 2010 260 http://www.omg.org/spec/SysML/1.2/PDF 17 April 2012
- Object Management Group (OMG) 2010b SysMLModelica Transformation Specification Draft USA OMG 2010 101 http://www.omgwiki.org/OMGSysML/lib/exe/fetch.php?id=sysmlmodelica%3Asysml_and_modelica_integration&cache=cache&media=sysml-modelica:sysmlmodelica_xformspec_v.1.0_2010-5-10.pdf 17 April 2012
- Ogata, Katsuhiko 2009 Modern Control Engineering Fifth
- OPENMODELICA 2012 OPENMODELICA Site http://www.openmodelica.org/ 01 April 2012
- MODELICA Association 2012 Modelica Language Specification: Version 3.2R1 https://www.modelica.org/news_items/documents/ModelicaSpec32Revision1.pdf 17 April 2012
- Redman, D. Ward, D. Chilenski, J. Pollari, G. 2010 Virtual Integration for Improved System Design In proceeding… The First Analytic Virtual Integration of Cyber-Physical Systems Workshop San Diego, California: USA
- Santiago, V. Vijaykumar, N. L. Guimaraes, D. Amaral, D.S. Ferreira, E. 2008 An environment for automated test case generation from statechart-based and finite state machine-based behavioral models In proceedings… 2008 IEEE International Conference on Software Testing Verification and Validation Workshop Washington, DC, USA IEEE Computer Society 2008 63 72
- SCICOSLAB 2012 SCICOSLAB Site http://www.scicoslab.org/ 01 April 2012
- Shah, A. A. Kerzhner, A. A. Shaefer, D. Paredis, C. J. J. 2010 Multi-View Modeling to Support Embedded Systems Engineering in SysML Lecture Notes in Computer Science, Graph Transformations and Model-Driven Engineering 2010 5765 2010 580 601
- Simao, A.S. Ambrosio, A.M. Fabri, S.C.P.F. Amaral, A.M.S. Martins, E. Maldonado, J.C. 2005 Plavis/FSM: an environment to integrate FSM-based testing tools Simpósio Brasileiro de Engenharia de Software - Sessão de Ferramentas, 19. SBES 2005 3 7 outubro 2005 Uberlândia, MG Universidade Federal de Uberlândia
- Thramboulidis, K. 2010 The 3 + 1 SysML View-Model in Model Integrated Mechatronics Journal of Software Engineering and Applications 3 2 2010 109 118
- TOPCASED 2012 TOPCASED Site http://www.topcased.org 01 April 2012