Description
HyMITATOR is a tool dedicated to the synthesis of parameters for hybrid automata (HA). It is a fork of IMITATOR, the tool for parameter synthesis in timed automata.
HyMITATOR implements extensions of the inverse method [ACEF09] and the behavioral cartography [AF10], initially defined for parametric timed automata, and adapted to hybrid automata [FK11]. In particular, it generalizes a concrete behavior of a HA, by synthesizing constraints on the parameters guaranteeing the same time-abstract behavior.
HyMITATOR is fully written in OCaml, and is available under the GNU General Public License.
Features
HyMITATOR implements the following features:
- On-the-fly computation of the parametric reachability graph
- Predicate Abstraction: Safety verification can alternatively be performed using a counterexample-guided abstraction refinement loop. The abstract state space is constructed w.r.t. a set of linear predicates.
- Implementation of the inverse method for Hybrid Automata [ACEF09], [FK11]
- Implementation of the behavioral cartography algorithm for HAs [AF10], [FK11]
The execution of HyMITATOR is fully automated, from the source file to the generation of the behavioral tiles and the corresponding trace sets under a graphical form.
The Team
HyMITATOR has been originally developed at LSV.
Main contributors:
