|HAT: Analyze the Linear Hybrid Automata As a Labelled Transition System|
|This website is a preliminary simple version for the review.|
HAT is a tool which can transform an LHA model into equivalent LTS model. Then users can use off-the-shelf LTS checkers to answer considerably difficult questions about the behavioral state space of LHA easily. So far, HAT supports the interaction with three mature LTS checkers which are, ARMC for both reachability analysis and termination analysis, Invgen and interproc for invariant generation.
Please download the tool HAT from this link.
Notice: In order to perform the selected functionalities, please download and install the related LTS checkers and configure the directory of these tools in HAT in advance. You may download ARMC from here, download Invgen from here. For Interproc, as we slightly modified Interproc to make it available to accept the LTS files, please download our modified version from here. In order to run Interproc, you may need to install all the required library files for Interproc in advance.
The ha files we used in the experiment can download here
Here is the model we use inthe experiment
ARMC Based Reachability Checking Result
ARMC Based Termination Analysis Result
Interproc Based Invariant Generation Result
ARMC Based Reachability Checking
ARMC Based Termination Analysis
Interproc Based Invariant Generation