Academic
Publications
Path-oriented bounded reachability analysis of composed linear hybrid systems

Path-oriented bounded reachability analysis of composed linear hybrid systems,10.1007/s10009-010-0163-9,International Journal on Software Tools for Te

Path-oriented bounded reachability analysis of composed linear hybrid systems   (Citations: 2)
BibTex | RIS | RefWorks Download
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.
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...• A new encoding is introduced for checking the pathoriented reachability problem of a path set [7]...
    • ...Instead of using the above two methods, in BACH 2 we implement our path-oriented reachability analysis method [7] which encodes each path in a path set separately and controls the synchronization by adding a special group of constraints...

    Lei Buet al. BACH 2 : Bounded reachability checker for compositional linear hybrid ...

Sort by: