Design Principles for an Extendable Verification Tool for Hybrid Systems
Design Principles for an Extendable Verification Tool for Hybrid Systems
复制标题
DOI：
10.3182/20090916-3-es-3003.00043
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
Goran Frehse;Rajarshi Ray
中科院分区：
文献类型：
--
作者：
Goran Frehse;Rajarshi Ray
摘要连续和混合系统的验证是困难的，今天的工具仅限于相对较小的问题。目前正在研究几种新的方法，利用各种集合表示（多面体，zonotopes），改进的算法（避免包装效果）和策略（如抽象细化）。我们概述了一个工具框架，能够集成和联合收割机从这些方法的不同元素。该框架包括常见功能（混合自动机，图形输出，基本集合操作等）的实现。以及允许我们插入不同实现的接口，例如特定类型的集合表示或特定的优化算法。这使我们能够实验性地评估竞争的想法，联合收割机有前途的元素和探索新的方法，相对较少的开发工作。
Abstract The verification of continuous and hybrid systems is known to be hard, and today tools are limited to relatively small problems. Several novel approaches are currently under investigation that exploit various kinds of set representations (polyhedra, zonotopes), improved algorithms (avoiding the wrapping effect) and strategies (such as abstraction refinement). We outline a tool framework that is able to integrate and combine different elements from these approaches. The framework includes implementations for common functionality (hybrid automata, graphical output, basic set operations, etc.) and interfaces that allow us to plug in different implementations, such as a particular kind of set representation or a particular optimization algorithm. This allows us to experimentally evaluate competing ideas, combine promising elements and explore new approaches with relatively little development effort.