Path-oriented bounded reachability analysis of composed linear hybrid systems |
| |
Authors: | Lei Bu Xuandong Li |
| |
Affiliation: | 1.State Key Laboratory of Novel Software Technology,Nanjing University,Nanjing,People’s Republic of China;2.Department of Computer Science and Technology,Nanjing University,Nanjing,People’s Republic of China |
| |
Abstract: | 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. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|