BACH: Bounded reAchablity CHecker
Introduction Download Case Studies SnapShots BACH Team

Introduction

Overview  

BACH stands for Bounded reAcheability CHecker, it is a bounded model checker for Linear Hybrid Systems. BACH was designed and implemented by Software Engineering Group, Nanjing University.

In BACH, we provide the following functionality:

1.Graphical LHA Editor: It allows users to construct, edit, and perform syntax analysis of LHA interactively. This Editor can also save the graphical representation of LHA to a human readable text file which is used as the input file for reachability checker.

2.Bounded Reachabilty Cheker: It accepts a LHA file generated by the Editor, and perform the bounded reachability
checking. BACH supports two kinds of reachability checking:

2.1 Path-Oriented Reachability Checker: The checker requires users to select a specific path set, which include one path for each component respectively, and use the method presented in this paper to check the reachability of this path set.

2.2 Bounded Reachability Checker: This checker uses the path-oriented checker as underlying solver. It traverses all the path sets in the threshold by a tailored Depth-First Search algorithm, and check the related path set for reachability using linear programming to perform bounded reachability checking.

 

We have a special edition of BACH: BACHOL, which supports the online modeling and verification of linear hybrid automata. By retaining all the functionality of BACH, BACHOL also supports the following functionalities: .

1. Graphical Editor for LHA Template: We allow to build a LHA template which is a LHA with free parameters included, in the format of ".hat".

2. Online Modeling and Verification Module: This module reads the LHA template and scripts which include concrete parameter values and reachability specifications from user. Then the template will be concretized to a standard LHA according to the values provided and an automatic reachability verification will be performed according to the specification given in the script.

A preliminary demo of using BACHOL in the online modeling and verification of a communication based train control system is available from this link. More demos will be available soon.

 

 

Documentation

  • Yang Yang, Lei Bu, Xuandong Li. Forward and Backward: Bounded Model Checking of Linear Hybrid Automata From Two Directions. In Proceedings of the 12th International Conference on Formal Methods in Computer Aided Design (FMCAD2012), USA, IEEE Computer Society Press, 2012.

  • Lei Bu, Yang Yang, Xuandong Li. IIS-Guided DFS for Efficient Bounded Reachability Analysis of Linear Hybrid Automata. In Proceedings of Haifa Verification Conference (HVC 2011), Israel, Lecture Notes in Computer Science 7261, Springer, 2012, pp.35-49.

  • Lei Bu, You Li, Linzhang Wang and Xuandong Li. BACH : Bounded ReachAbility CHecker for Linear Hybrid Automata. In Proceedings of the 8th International Conference on Formal Methods in Computer Aided Design(FMCAD2008). Portland, OR, USA, IEEE Computer Society Press, pp.65-68, 2008.

  • Lei Bu and Xuandong Li. Path-Oriented Bounded Reachability Analysis of Composed Linear Hybrid Systems, In International Journal on Software Tools for Technology Transfer, Springer, to appear.

  • Lei Bu, You Li, Linzhang Wang, Xin Chen, and Xuandong Li. BACH 2: Bounded ReachAbility CHecker for Compositional Linear Hybrid System, In Proceeding of the 13th Design Automation & Test in Europe Conference, Dresden, Germany, pp. 1512-1517, 2010.

  • User Manual for version before BACH 1.0(PRC UserManual).

 

Download

You may download BACH and BACHOL via the download page.

The current version of BACH is BACH-SAT.

 

We also provide details of two well-known examples . They can be found in the case studies page.

 

 

©2009 SEG CS NJU IntroductionDownloadCaseStudiesSnapShots