An expressive input language
IMITATOR performs parameter synthesis for real-time systems modeled by an extension of parametric timed automata.
My software
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.
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.
Other software
PAT
Member of the development team (2010-2013)
PAT is a powerful model-checker for multiple formalisms such as timed CSP, probabilistic systems, parametric systems… PAT is mainly developed in Singapore (NUS, STUD, NTU).
PolyOp
Developer
PolyOp is a simple interface to some operations on polyhedra provided by the Parma Polyhedra Library.
PSyHCoS
Developer
PSyHCoS is tool that groups techniques of parameter synthesis for Parametric Stateful Timed CSP (PSTCSP).
HyMITATOR
Developer
HyMITATOR is a fork of IMITATOR for parametric hybrid automata.
InSPEQTor
Developer
InSPEQTor is an implementation of the inverse method in the framework of Parametric Directed Weighted Graphs.
ImpRator
Developer
ImpRator is an implementation of the inverse method in the framework of Parametric Markov Decision Processes.