Assume-guarantee verification of nonlinear hybrid systems with ARIADNE
Assume-guarantee verification of nonlinear hybrid systems with ARIADNE
复制标题
DOI：
10.1002/rnc.2914
复制
发表时间：
2014-03-10
影响因子：
3.9
通讯作者：
Villa, Tiziano
中科院分区：
文献类型：
--
作者：
Benvenuti, Luca;Bresolin, Davide;Villa, Tiziano
在许多应用领域中，需要对具有混合离散和连续行为的复杂系统进行建模和设计，这些复杂系统不能仅使用离散或连续模型来忠实地表征。这样的系统由一个在连续环境中运行的离散控制部分组成，由于它们的混合性质而被命名为混合系统。不幸的是，大多数混合系统的验证问题，如可达性分析，变成不可判定的。正因为如此，在文献中已经提出了许多近似技术和工具来估计可达集。然而，大多数工具无法处理非线性动力学和约束，并且具有限制性许可证。为了克服这些局限性，我们最近提出了一个开源的混合系统验证框架，称为Ariadne，它利用近似技术的基础上实现形式验证算法的可计算分析理论。在本文中，我们将展示如何近似能力的Ariadne可以用来验证复杂的混合动力系统，采用假设保证推理方法。版权所有（c）2012约翰威利父子有限公司
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. Copyright (c) 2012 John Wiley & Sons, Ltd.