BACH: A toolset for bounded reachability analysis of linear hybrid systems

作者：Bu Lei^*; Li You; Wang Lin Zhang; Li Xuan Dong

来源：Journal of Software, 2011, 22(4): 640-658.

DOI：10.3724/SP.J.1001.2011.03766

• Common problems
• Design engineers
• Experiment data
• Linear hybrid automata
• Linear hybrid system
• Linear hybrid systems
• Model checking problem
• Problem size
• Reachability
• Reachability analysis
• State space
• Toolsets

The model-checking problem for hybrid systems is very difficult to resolve. Even for a relatively simple class of hybrid systems, the class of linear hybrid automata, the most common problem of reachability is unsolvable. Existing techniques for the reachability analysis of linear hybrid automata do not scale well to problem sizes of practical interest. Instead of developing a tool to perform a reachability checking of the complete state space of linear hybrid automata, a prototype toolset BACH (bounded reachability checker) is presented to perform path-oriented reachability checking and bounded reachability checking of the linear hybrid automata and the compositional linear hybrid systems, where the length of the path being checked can be made very large, and the size of the system can be made large enough to handle problems of practical interest. The experiment data shows that BACH has good performance and scalability and supports the fact that BACH can become a powerful assistant for design engineers in the reachability analysis of linear hybrid automata.

• 出版日期2011
• 单位南京大学