HARE: A Hybrid Abstraction Refinement Engine for Verifying Non-linear Hybrid Automata
HARE: A Hybrid Abstraction Refinement Engine for Verifying Non-linear Hybrid Automata
复制标题
HARE：用于验证非线性混合自动机的混合抽象细化引擎
DOI：
--
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Mahesh Viswanathan
中科院分区：
文献类型：
--
作者：
Nima Roohi;P. Prabhakar;Mahesh Viswanathan
混合抽象-精化引擎（Hybrid Abstraction-Refinement Engine，简称CEGAR）是一种基于反例引导的抽象-精化工具，用于验证混合自动机的安全性。混合自动机在每种模式下的连续动力学都是非线性的，但其初始值、不变量和转换关系都是使用多面体约束指定的。新窗口中的Open Image通过将非线性混合自动机抽象为多面体包含动力学混合自动机，并利用新窗口中的Open Image对反例进行验证。我们表明，CEGAR框架形成的理论基础，在新窗口中打开图像，使可证明的进展，在每次迭代的抽象-细化循环。当前的Open image in new window工具是以前版本的Open image in new window的一个重大进步-它考虑了更丰富的抽象模型类别（多面体流而不是矩形流），并且可以应用于更大类别的具体模型（非线性混合自动机而不是仿射混合自动机）。这些进步为更广泛的示例类带来了更好的性能结果。我们报告了在新窗口中打开图像与仿射模型（在新窗口中打开图像，在新窗口中打开图像，在新窗口中打开图像）和非线性模型（在新窗口中打开图像，在新窗口中打开图像，在新窗口中打开图像）的其他最先进的工具的实验比较。
Open image in new window (Hybrid Abstraction-Refinement Engine) is a counterexample guided abstraction-refinement (CEGAR) based tool to verify safety properties of hybrid automata, whose continuous dynamics in each mode is non-linear, but initial values, invariants, and transition relations are specified using polyhedral constraints. Open image in new window works by abstracting non-linear hybrid automata into hybrid automata with polyhedral inclusion dynamics, and uses Open image in new window to validate counterexamples. We show that the CEGAR framework forming the theoretical basis of Open image in new window , makes provable progress in each iteration of the abstraction-refinement loop. The current Open image in new window tool is a significant advance on previous versions of Open image in new window —it considers a richer class of abstract models (polyhedral flows as opposed to rectangular flows), and can be applied to a larger class of concrete models (non-linear hybrid automata as opposed to affine hybrid automata). These advances have led to better performance results for a wider class of examples. We report an experimental comparison of Open image in new window against other state of the art tools for affine models ( Open image in new window , Open image in new window , and Open image in new window ) and non-linear models ( Open image in new window , Open image in new window , and Open image in new window ).