Assume–guarantee verification of nonlinear hybrid systems with Ariadne

• DOI: 10.1002/rnc.2914
• Publication Date: 2012-10-11T19:13:33Z
• Authors: Luca Benvenuti; Davide Bresolin; Pieter Collins; Alberto Ferrari; Luca Geretti; Tiziano Villa
• Keywords: Undecidable problem

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