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

Snapshots for the latest version (BACH-SAT)

LHA_Checker: The component of Checking part which can process one automata. It can check the reachablity of one location in a linear hybrid automata. This version supports changing the LP solving algorithm used by CPLEX.

 

 


Snapshots for version (BACH 2.1)

This edition of BACH is composed of three main parts.

 

1.HA_Editor: It is the component for graphical representation of the automata, and it can generate the textual edition (*.ha) of the object hybrid system automaticallly, with some pre syntax checking.

 

 

2.LHA_Checker: The component of Checking part which can process one automata.It can check the reachablity of one path, or check the reachability of the location(s) and transition(s) in a linear hybrid automata.

 

3.CLHA_Checker: The component of Checking part which can process compositional LHA systems.It can check the path-oriented reachability of compositional LHA systems, or check the bounded reachability of the location in compositional LHA systems.

 

 


©2009 SEG CS NJU IntroductionDownloadCaseStudiesSnapShots