Hierarchical Analysis of Hybrid Automata
The verification tool HAHA (Hierarchical Analysis of Hybrid Automata) implements an algorithm for safety verification of unbounded uniform systems of linear automata.
It employs an extension of the hierarchical theorem prover H-PILoT to reduce the verification problem to ground satisfiability problems in the base theory of linear real arithmetic with free function symbols.
These problems are then checked by an SMT prover.
We use an XML format to describe hybrid automata, or families thereof. To analyze an automaton, execute the following command:
The following command line options are available:
- --use-mode-reachability: Do the verification for mode-reachable states only.
- --produce-latex-output: Output the results as a LaTeX table.
- --prover PROV: Select an SMT prover. Possible values are Z3 (the default), CVC, and Redlog.
- -o DIR or
--output-directory DIR: Set the output directory. Default: 'output'
- --only-translation: Do not hand over to H-PILoT, just produce .loc files.
- --only-reduction: Do not hand over to an SMT prover, just produce SMT-LIB files.
- --runs RUNS: Set the number of times the verification is repeated for the statistics. Default is 1.
- --verbosity VER: Set the verbosity level, from taciturn (0) to garrulous (2). Default is 0.
- --version: Print version number.
- -help or
--help: Display this list of options
The development version of the tool and its sources are available upon request.
We collected the raw data for the experiments described in our submitted paper in a tgz archive in May 2015.
This archive contains
- a README file containing detailed usage information
- a description of the hybrid automaton of our running example (example.xml)
- a description of problems from the benchmark suite of the Passel tool by Johnson/Mitra (fischer*.xml, simple-sats.xml, sats-ii-harder-sides.xml)
- executables of the tools that can be used to repeat our experiments:
- z3, an SMT solver (z3.codeplex.com)
- H-PILoT, which performs the hierarchical reduction to an SMT problem (userpages.uni-koblenz.de/~sofronie/hpilot/)
- HAHA converts an automaton description into a list of verification problems, calls H-PILoT and produces statistics
a subfolder "intermediate_results" with
the formalizations of haha for H-PILoT and
the SMT problems created by H-PILoT for Z3.
All executables are included in a windows variant (.exe) as well as a unix variant.