Path-oriented bounded reachability analysis of composed linear hybrid systems

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 effi...

Full description

Saved in:
Bibliographic Details
Published in:International journal on software tools for technology transfer 2011-08, Vol.13 (4), p.307-317
Main Authors: Bu, Lei, Li, Xuandong
Format: Article
Language:English
Subjects:
Applied sciences
Automation
Checkers
Computer programs
Computer Science
Computer science
control theory
systems
Computer systems performance. Reliability
Design engineering
Dynamical systems
Exact sciences and technology
Explosions
Hybrid systems
Linear programming
Regular Paper
Software
Software Engineering
Software Engineering/Programming and Operating Systems
Solvers
Tasks
Theory of Computation
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:1433-2779
1433-2787
DOI:10.1007/s10009-010-0163-9