IMITATOR: parameter synthesis for real-time systems
I initated the development of IMITATOR in 2008, and I am since then the lead developer.
IMITATOR is a software to synthesize timing parameters for concurrent timed systems modeled using extensions of parametric timed automata.
IMITATOR was used in several industrial collaborations on hardware verification, and schedulability analysis under uncertainty.
An expressive input language
IMITATOR performs parameter synthesis for real-time systems modeled by an extension of parametric timed automata.
Powerful analyses
Various algorithms are implemented in IMITATOR, including safety parameter synthesis, deadlock-freeness, non-Zeno parametric model-checking or robustness analysis.
Graphical outputs
In addition to results output using predefined formats, IMITATOR generates graphical outputs such as the zones of good behaviors for the timing parameters.
Open source
IMITATOR is entirely open-source and is distributed under the GNU General Public License.
