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

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.

 

We have another special edition of BACH: BRICK, which is a bounded reachability checker for numerically intensive C code, with special emphasis on handling nonlinear operations. In BRICK, we provide the following functionalities:

1. Path-Oriented Bounded Reachability Checker: The checker enumerates all paths within user-specified search depth, and checks their reachability by underlying solvers as well as some optimization algorithms.

2. Checking of codes with nonlinear operations: BRICK supports the solving of nonlinear constraints generated from path conditions, e.g. trigonometric functions, exponential functions by delta-decision SMT solving and derivative-free optimization.

A preliminary version of BRICK can be found at this link.

 

Documentation

  • Yuming Wu, Lei Bu, Jiawan Wang, Xinyue Ren, Wen Xiong, and Xuandong Li. 2022. Mixed Semantics Guided Layered Bounded Reachability Analysis of Compositional Linear Hybrid Automata. In Verification, Model Checking, and Abstract Interpretation: 23rd International Conference, VMCAI 2022, Philadelphia, PA, USA, January 16–18, 2022, Proceedings. Springer-Verlag, Berlin, Heidelberg, 473–495.

  • Jiawan Wang, Lei Bu, Shaopeng Xing, Yuming Wu, and Xuandong Li. 2021. Combined Online Checking and Control Synthesis: A Study on a Vehicle Platoon Testbed. In Formal Methods: 24th International Symposium, FM 2021, Virtual Event, November 20–26, 2021, Proceedings. Springer-Verlag, Berlin, Heidelberg, 752–762.

  • Shaopeng Xing, Jiawan Wang, Lei Bu, Xin Chen, and Xuandong Li. 2021. Approximate optimal hybrid control synthesis by classification-based derivative-free optimization. In Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control (HSCC '21). Association for Computing Machinery, New York, NY, USA, Article 7, 1–11.

  • Jiawan Wang, Lei Bu, Shaopeng Xing and Xuandong Li. 2021. PDF: Path-Oriented, Derivative-Free Approach for Safety Falsification of Nonlinear and Nondeterministic CPS," in IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 41, no. 2, pp. 238-251.

  • Lei Bu, Qixin Wang, Xinyue Ren, Shaopeng Xing and Xuandong Li. 2019. Scenario-Based Online Reachability Validation for CPS Fault Prediction," in IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 39, no. 10, pp. 2081-2094.

  • Lei Bu, Jiawan Wang, Yuming Wu, and Xuandong Li. 2019. From Bounded Reachability Analysis of Linear Hybrid Automata to Verification of Industrial CPS and IoT. In Engineering Trustworthy Software Systems: 5th International School, SETSS 2019, Chongqing, China, April 21–27, 2019, Tutorial Lectures. Springer-Verlag, Berlin, Heidelberg, 10–43.

  • Lei Bu, Shaopeng Xing, Xinyue Ren, Yang Yang, Qixin Wang and Xuandong Li. 2019. Incremental Online Verification of Dynamic Cyber-Physical Systems," 2019 Design, Automation & Test in Europe Conference & Exhibition (DATE), 2019, pp. 782-787.

  • Dingbao Xie, Wen Xiong, Lei Bu, and Xuandong Li. 2017. Deriving Unbounded Reachability Proof of Linear Hybrid Automata during Bounded Checking Procedure. IEEE Trans. Comput. 66, 3 (March 2017), 416–430.

  • Dingbao Xie, Lei Bu, and Xuandong Li. Deriving Unbounded Proof of Linear Hybrid Automata from Bounded Verification. 2014. IEEE Real-Time Systems Symposium, 2014, pp. 128-137.

  • Dingbao Xie, Lei Bu, Jianhua Zhao, and Xuandong Li. 2014. SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata. Form. Methods Syst. Des. 45, 1 (August 2014), 42–62.

  • 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 5.5.

 

We provide repeatibility evaluation for the ARCH-COMP 2022 category report: Artificial intelligence and neural network control systems (AINNCS) for continuous and hybrid systems plants of the 6th International Competition on Verifying Continuous and Hybrid Systems (ARCH-COMP '22). They can be found in the competition page.

 

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

 

 
©2009 SEG CS NJU Introduction• Download• CaseStudies• SnapShots• Competition