Extending model checkers for hybrid system verification: the case study of SPIN. (26th July 2013)

• Record Type: Journal Article
• Authors: Gallardo, María‐del‐Mar; Panizo, Laura
• Is Part Of: Software testing, verification & reliability. Volume 24:Number 6(2014)
• Page Start: 438
• Page End: 471
• Publication Date: 2013-07-26
• Subjects: Computer software -- Testing -- Periodicals; Computer software -- Verification -- Periodicals; Computer software -- Reliability -- Periodicals; 005.14
• DOI: 10.1002/stvr.1505
• Languages: English
• ISSNs: 0960-0833

Abstract

<abstract abstract-type="main" id="stvr1505-abs-0001"> <title>SUMMARY</title> <p id="stvr1505-para-0001">A hybrid system is a system that evolves following a continuous dynamic, which may instantaneously change when certain internal or external events occur. Because of this combination of discrete and continuous dynamics, the behaviour of a hybrid system is, in general, difficult to model and analyse. Model checking techniques have been proven to be an excellent approach to analyse 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 behaviour irrespective of the underlying model checker. The methodology is applied to <sc>SPIN</sc> using Parma Polyhedra Library. In addition, the authors are currently working on the extension of other model checkers. Copyright © 2013 John Wiley &amp; Sons, Ltd.</p> </abstract>