IMITATOR: synthèse de paramètres pour les systèmes temps-réel
J’ai créé l’outil IMITATOR en 2008, et suis depuis son principal développeur.
IMITATOR est un logiciel pour synthétiser des valeurs de paramètres temporels dans les systèmes temporisés concurrents modélisés par des extensions des automates temporisés paramétrés.
IMITATOR a été utilisé dans le cadre de plusieurs collaborations avec l’industrie, notamment pour la vérification de systèmes matériels et pour l’analyse d’ordonnancement en présence d’incertitude.
Un langage d’entrée expressif
IMITATOR effectue de la synthèse de paramètres pour les systèmes temps-réel modélisés par une extension des automates temporisés paramétrés.
Des analyses puissantes
Plusieurs algorithmes sont implémentés dans IMITATOR, dont la synthèse pour la sûreté, l’absence de deadlocks, le model-checking paramétré non-Zeno, ou encore l’analyse de robustesse.
Sorties graphiques
En plus des sorties normalisées, IMITATOR génère des sorties graphiques tells que les zones de bon fonctionnement des paramètres temporels.
Un logiciel libre
IMITATOR est entièrement libre et est distribué selon les termes de la licence publique générale GNU.
