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.
Développement logiciel
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.
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.
Autres logiciels
PAT
Membre de l’équipe de développement (2010-2013)
PAT est un model-checker puissant pour de multiples formalismes, dont timed CSP, les systèmes probabilistes, les systèmes paramétrés… PAT est principalement développé à Singapour (NUS, STUD, NTU).
PolyOp
Développeur
PolyOp est une interface simple pour encapsuler des opérations sur les polyèdres fournies par la bibliothèque PPL (Parma Polyhedra Library).
PSyHCoS
Développeur
PSyHCoS est un outil de synthèse de paramètres pour l’algèbre de processus Parametric Stateful Timed CSP (PSTCSP).
HyMITATOR
Développeur
HyMITATOR est une variante d’IMITATOR pour les automates hybrides paramétrés.
InSPEQTor
Développeur
InSPEQTor est une implémentation de la méthode inverse pour les graphes orientés valués paramétrés.
ImpRator
Développeur
ImpRator est une implémentation de la méthode inverse pour les processus de décision markoviens paramétrés.