RT Journal Article
T1 Extending model checkers for hybrid system verification: the case study of SPIN.
A1 Gallardo-Melgarejo, María del Mar
A1 Panizo-Jaime, Laura
K1 Sistemas de control inteligente
K1 Sistemas expertos - Verificación
K1 Dinámica
AB A hybrid system is a system that evolves following a continuous dynamic, which may instantaneously change when certain internal or external events occur. Due to this combination of discrete and continuous dynamics, the behavior of a hybrid system is, in general, difficult to model and analyze. Model checking techniques have been proven to be an excellent approach to analyze critical properties of complex systems.This paper presents a new methodology to extend explicit model checkers for hybrid systems analysis. The explicit model checker is integrated, in a non-intrusive way, with some external structures and existing abstraction libraries, which store and manipulate the abstraction of the continuous behavior irrespectiveof the underlying model checker. The methodology is applied to SPIN using Parma Polyhedra Library. In addition, the authors are currently working on the extension of other model checkers.
PB Willey
YR 2013
FD 2013-07-26
LK https://hdl.handle.net/10630/31011
UL https://hdl.handle.net/10630/31011
LA eng
NO Gallardo, M., & Panizo, L. (2014). Extending model checkers for hybrid system verification: the case study of <scp>SPIN</scp>. Software Testing, Verification and Reliability, 24(6), 438–471.
NO This work has been funded by Spanish projects TIN 2008-05932 and IPT-2011-1034-370000, by the Andalusian project P11-TIC4659 and ERDF from the European Commission.
DS RIUMA. Repositorio Institucional de la Universidad de Málaga
RD 21 ene 2026