HAT: Analyze the Linear Hybrid Automata As a Labelled Transition System
This website is a preliminary simple version for the review.

Overview  

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.

 

Download

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.  

 

Case Studies

The ha files we used in the experiment can download here

Here is the model we use inthe experiment

WLM

Interproc Based Invariant Generation

TCS

Interproc Based Invariant Generation

Motor

Interproc Based Invariant Generation

ARMC Based Reachability Checking Result

Name Time
WLM 0.63s
TCS 0.84s
Motor5 0.42s
Motor10 2.05s
Motor20 16.41s
Motor30 77.53s
Motor50 628.74s
Motor60 1501.93s
Motor70 3087.63s
Motor78 N/A

 

ARMC Based Termination Analysis Result

Name Time Name Time
WLM
4.74s
WLM-tmnt
1.60s
TCS
0.69s
TCS-tmnt
0.76s
Motor5
1.45s
Motor5-tmnt
0.58s
Motor6
2.63s
Motor6-tmnt
0.79s
Motor7
4.12s
Motor7-tmnt
0.30s
Motor8
5.77s
Motor8-tmnt
0.98s
Motor9
9.54s
Motor9-tmnt
0.84s
Motor10
15.32s
Motor10-tmnt
0.67s
Motor20
1455.65s
Motor20-tmnt
2.00s
Motor30
N/A
Motor30-tmnt
3.78s
Motor40
N/A
Motor40-tmnt
7.45s
Motor50
N/A
Motor50-tmnt
14.84s
Motor60
N/A
Motor60-tmnt
25.36s
Motor100
N/A
Motor100-tmnt
142.52s

 

Interproc Based Invariant Generation Result

Name Box Octagon PPL
WLM 0.40s 0.31s 0.97s
TCS 0.40s 0.94s 0.82s
Motor3 0.34s 0.26s 0.15s
Motor4 0.58s 0.88s 0.54s
Motor5 0.44s 0.64s 3.21s
Motor6 0.47s 0.74s 42.53s
Motor7 0.52s 1.26s 2082.48s
Motor8 0.58 1.47s N/A
Motor9 0.66s 2.25s N/A
Motor10 0.76s 3.15s N/A
Motor20 1.17s 34.16s N/A
Motor30 1.22s 180.29s N/A
Motor40 2.31s N/A N/A
Motor50 4.04s N/A N/A
Motor60 6.16s N/A N/A
Motor100 26.17s N/A N/A

Snapshots

ARMC Based Reachability Checking

ARMC Based Reachability Checking

 

ARMC Based Termination Analysis

ARMC Based Termination Analysis

 

Interproc Based Invariant Generation

Interproc Based Invariant Generation

 

 

 

 

 

©2014