Assume-guarantee verification of nonlinear hybrid systems with ARIADNE.

*(English)*Zbl 1284.93121Summary: 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 ARIADNE, 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 ARIADNE can be used to verify complex hybrid systems, adopting an assume-guarantee reasoning approach.

##### MSC:

93C30 | Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) |

93B15 | Realizations from input-output data |

93C10 | Nonlinear systems in control theory |

PDF
BibTeX
XML
Cite

\textit{L. Benvenuti} et al., Int. J. Robust Nonlinear Control 24, No. 4, 699--724 (2014; Zbl 1284.93121)

Full Text:
DOI

##### References:

[1] | Alur, The algorithmic analysis of hybrid systems, Theoretical Computer Science 138 pp 3– (1995) · Zbl 0874.68206 |

[2] | Maler, Real-time: Theory in Practice 600 pp 447– (1991) |

[3] | Collins, Continuity and computability of reachable sets, Theoretical Computer Science 341 pp 162– (2005) · Zbl 1154.93351 |

[4] | Yovine, Kronos: ass verification tool for real-time systems, International Journal on Software Tools for Technology Transfer 1 (1-2) pp 123– (1997) · Zbl 1060.68606 |

[5] | Larsen, UPPAAL in a nutshell, International Journal on Software Tools for Technology Transfer 1 (1-2) pp 134– (1997) · Zbl 1060.68577 |

[6] | Henzinger, HYTECH: a model checker for hybrid systems, International Journal on Software Tools for Technology Transfer 1 (1-2) pp 110– (1997) · Zbl 1060.68603 |

[7] | Asarin, CAV ’02: Proceedings of the 14th International Conference on Computer Aided Verification pp 365– (2002) |

[8] | Botchkarev, Proceedings of Hybrid Systems: Computation and Control (HSCC’00), LNCS 1790 pp 73– (2000) |

[9] | Tiwari, Abstractions for hybrid systems, Formal Methods in System Design 32 (1) pp 57– (2008) · Zbl 1133.68368 |

[10] | Frehse, Phaver: algorithmic verification of hybrid systems past hytech, International Journal on Software Tools for Technology Transfer (STTT) 10 pp 263– (2008) · Zbl 05536139 |

[11] | Frehse, Proceedings of the 23rd International Conference on Computer Aided Verification (CAV 2011), LNCS 6806 pp 379– (2011) |

[12] | Clarke, Abstraction and counterexample-guided refinement in model checking of hybrid systems, International Journal of Foundations of Computer Science 14 (4) pp 583– (2003) · Zbl 1101.68678 |

[13] | Ratschan, Safety verification of hybrid systems by constraint propagation based abstraction refinement, ACM Transactions in Embedded Computing Systems (2007) · Zbl 05452349 |

[14] | Platzer, Lecture Notes in Computer Science 5195, in: Proceedings of the Third International Joint Conference on Automated Reasoning (IJCAR 2008) pp 171– (2008) · Zbl 1165.68469 |

[15] | Donzé, Lecture Notes in Computer Science 6174, in: Computer Aided Verification pp 167– (2010) · Zbl 05772630 |

[16] | Dellnitz, Ergodic Theory, Analysis, and Efficient Simulation of Dynamical Systems pp 145– (2001) |

[17] | Makino, Cosy infinity version 9, Nuclear Instruments and Methods A558 pp 346– (2006) |

[18] | Tomlin, Computational techniques for the verification of hybrid systems, Proceedings of the IEEE 91 (7) pp 986– (2003) |

[19] | Weihrauch, Computable Analysis - An Introduction (2000) · Zbl 0956.68056 |

[20] | Ariadne: an open tool for hybrid system analysis http://ariadne.parades.rm.cnr.it |

[21] | Lynch, Hybrid I/O automata, Information and Computation 185 (1) pp 105– (2003) · Zbl 1069.68067 |

[22] | Henzinger, What’s decidable about hybrid automata?, Journal of Computer and System Sciences 57 (1) pp 94– (1998) · Zbl 0920.68091 |

[23] | Collins P Computable analysis with applications to dynamic systems Technical Report MAC-1002 2010 http://oai.cwi.nl/oai/asset/16557/16557D.pdf |

[24] | Benvenuti, HSCC ’08: Proceedings of the 11th International Workshop on Hybrid Systems, LNCS 4981 pp 58– (2008) |

[25] | Collins, Semantics and computability of the evolution of hybrid systems, SIAM Journal on Control and Optimization 49 pp 890– (2011) · Zbl 1217.93024 |

[26] | Collins P Lygeros J Computability of finite-time reachable sets for hybrid systems Proceedings of the 44th IEEE Conference on Decision and Control 2005 4688 4693 |

[27] | Goebel, Solutions to hybrid inclusions via set and graphical convergence with stability theory applications, Automatica 42 (4) pp 573– (2006) · Zbl 1106.93042 |

[28] | Brattka, New Computational Paradigms pp 425– (2008) |

[29] | Li, An Introduction to Kolmogorov Complexity and Its Applications (2008) · Zbl 1185.68369 |

[30] | Balluchi A Casagrande A Collins P Ferrari A Villa T Sangiovanni-Vincentelli A Ariadne: a framework for reachability analysis of hybrid automata Proceedings of the 17th International Symposium on Mathematical Theory of Networks and Systems (MTNS 2006) 2006 1259 1267 |

[31] | Benvenuti L Bresolin D Casagrande A Collins P Ferrari A Mazzi E Sangiovanni-Vincentelli A Villa T Reachability computation for hybrid systems with Ariadne Proceedings of the 17th IFAC World Congress 2008 8960 8965 |

[32] | Collins P Bresolin D Geretti L Villa T Computing the evolution of hybrid systems using rigorous function calculus Proceedings of the 4th IFAC Conference on Analysis and Design of Hybrid Systems (ADHS12) 2012 284 290 |

[33] | Bryant, Graph-based algorithms for boolean function manipulation, IEEE Transactions on Computers C-35 (8) pp 677– (1986) · Zbl 0593.94022 |

[34] | BuDDy: a BDD package http://buddy.sourceforge.net/ |

[35] | Gössler, Lecture Notes in Computer Science 4362, in: SOFSEM 2007: Theory and Practice of Computer Science pp 295– (2007) · Zbl 1131.68474 |

[36] | Benvenuti L Ferrari A Mangeruca L Mazzi E Passerone R Sofronis C A contract-based formalism for the specification of heterogeneous systems Proceedings of the Forum on Specification, Verification and Design Languages FDL’08 2008 142 147 10.1109/FDL.2008.4641436 |

[37] | Rockafellar, Convex Analysis (1996) |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.