Path-oriented bounded reachability analysis of composed linear hybrid systems
Path-oriented bounded reachability analysis of composed linear hybrid systems
复制标题
DOI：
10.1007/s10009-010-0163-9
复制
发表时间：
2011-08
影响因子：
1.5
通讯作者：
Lei Bu;Xuandong Li
中科院分区：
文献类型：
--
作者：
Lei Bu;Xuandong Li
现有的线性混合系统的可达性分析技术不能很好地扩展到实际感兴趣的问题规模。现有的技术的性能更差的可达性分析的几个线性混合自动机的组合。本文提出了一种有效的面向路径的方法来分析由线性混合自动机建模的具有同步事件的组合系统的有界可达性。它适用于分析多部件系统，通过选择关键路径，而这一任务是相当难以克服的，因为以前的状态爆炸问题。这组路径将被转换成一组线性约束，可以有效地解决线性规划求解器。这种路径符号执行的方法允许设计工程师检查重要路径，并相应地增加对系统正确性的信心。这种方法被实现为一个原型工具Bounded reAchability Checker（BACH）。实验数据表明，无论是路径长度和参与自动机的数量在一个系统中使用BACH检查可以大大扩展，以满足实际需要。
The existing techniques for reachability analysis of linear hybrid systems do not scale well to the problem size of practical interest. The performance of existing techniques is even worse for reachability analysis of a composition of several linear hybrid automata. In this paper, we present an efficient path-oriented approach to bounded reachability analysis of composed systems modeled by linear hybrid automata with synchronization events. It is suitable for analyzing systems with many components by selecting critical paths, while this task was quite insurmountable before because of the state explosion problem. This group of paths will be transformed to a group of linear constraints, which can be solved by a linear programming solver efficiently. This approach of symbolic execution of paths allows design engineers to check important paths, and accordingly increase the faith in the correctness of the system. This approach is implemented into a prototype tool Bounded reAchability CHecker (BACH). The experimental data show that both the path length and the number of participant automata in a system checked using BACH can scale up greatly to satisfy practical requirements.