Assume–guarantee verification of nonlinear hybrid systems with Ariadne. (11th October 2012)

• Record Type: Journal Article
• Authors: Benvenuti, Luca; Bresolin, Davide; Collins, Pieter; Ferrari, Alberto; Geretti, Luca; Villa, Tiziano
• Is Part Of: International journal of robust and nonlinear control. Volume 24:Number 4(2014)
• Page Start: 699
• Page End: 724
• Publication Date: 2012-10-11
• Subjects: Automatic control -- Periodicals; Control theory -- Periodicals; Nonlinear systems -- Periodicals; 629.836
• DOI: 10.1002/rnc.2914
• Languages: English
• ISSNs: 1049-8923

Abstract

<abstract abstract-type="main" id="rnc2914-abs-0001"> <title>SUMMARY</title> <p id="rnc2914-para-0001">In many applicative fields, there is the need to model and design complex systems having a mixed discrete and continuous behavior that cannot be characterized faithfully using either discrete or continuous models only. Such systems consist of a discrete control part that operates in a continuous environment and are named hybrid systems because of their mixed nature. Unfortunately, most of the verification problems for hybrid systems, like reachability analysis, turn out to be undecidable. Because of this, many approximation techniques and tools to estimate the reachable set have been proposed in the literature. However, most of the tools are unable to handle nonlinear dynamics and constraints and have restrictive licenses. To overcome these limitations, we recently proposed an open‐source framework for hybrid system verification, called <sc>Ariadne</sc>, which exploits approximation techniques based on the theory of computable analysis for implementing formal verification algorithms. In this paper, we will show how the approximation capabilities of <sc>Ariadne</sc> can be used to verify complex hybrid systems, adopting an assume–guarantee reasoning approach. Copyright © 2012 John Wiley &amp; Sons, Ltd.</p> </abstract>