Projets-App
Projets
Editer un projet
Cadre de travail
Unité de recherche rattachée au CNRS
IRIF
LIPN
LMF
Information du ou de la responsable scientifique du projet :
Prénom
Nom
E-mail
Présentation du projet scientifique
Nom du project
Résumé publiable du projet (10 lignes max.)
IMITATOR est un outil de model-checking temporisé paramétré, permettant de synthétiser des valeurs de paramètres temporels pour lesquels une propriété est vérifiée. IMITATOR repose sur une bibliothèque de polyèdres, une structure de données très appropriée pour les modèles paramétrés. En revanche, pour les modèles *non* paramétrés (automates temporisés classiques, sans paramètres ni stopwatches), les polyèdres sont trop coûteux, et de simples DBMs (difference bound matrices) suffiraient amplement.
Champs thématiques adressés (séparés par des virgules)
Type
proof-of-concept
prototype
maintenance/évolution logiciel existant
prématuration
Décrivez les innovations attendues à l'issue du projet (5 lignes max.)
Pour les modèles *non* paramétrés (automates temporisés classiques, sans paramètres ni stopwatches), les polyèdres sont trop coûteux, et de simples DBMs (difference bound matrices) suffiraient amplement. Le projet consiste à offrir une structure modulaire pour les structures de données utilisées dans l'outil, dont le choix pourrait dépendre (automatiquement ou manuellement) des modèles d'entrée. D'autres structures que les DBMs et polyèdres pourraient ensuite être considérées (par exemple : DBMs paramétrées, zonotopes, octaèdres…).
Argumentaire scientifique qui décrit le projet, l'état de l'art, les travaux antérieurs et les résultats attendus (20 lignes max.)
IMITATOR est un outil de model checking temporisé paramétré, permettant de synthétiser des valeurs de paramètres temporels pour lesquels une propriété est vérifiée. Pour les modèles *non* paramétrés (automates temporisés classiques, sans paramètres ni stopwatches), les polyèdres sont trop coûteux, et de simples DBMs (difference bound matrices) suffiraient amplement. Le projet consiste à offrir une structure modulaire pour les structures de données utilisées dans l'outil, dont le choix pourrait dépendre (automatiquement ou manuellement) des modèles d'entrée. D'autres structures que les DBMs et polyèdres pourraient ensuite être considérées (par exemple : DBMs paramétrées, zonotopes, octaèdres…). Cela permettra d'améliorer d'un ou plusieurs ordres de magnitude l'efficacité d'IMITATOR sur les modèles les plus simples en termes de fonctionnalités (c'est-à-dire les moins expressifs) ; dans l'état actuel, des model-checkers non paramétrés (tels que Uppaal) sont d'un ordre de magnitude plus efficace que IMITATOR, ce qui est dommageable.
Description du besoin en ingénierie
Évaluez le temps ingénieur dont vous avez besoin pour votre projet:
Frequence
2 jour/semaine
3 jour/semaine
Durée
1 mois
2 mois
3 mois
4 mois
5 mois
6 mois
Quelles sont les compétences spécifiques d'ingénierie attendues ; notamment, langages ou frameworks qui seront utilisés dans le projet, outils existants, connaissances requises ?
OCaml Connaissances en automates appréciées, idéalement automates temporisés Connaissances en model-checking appréciées
Décrivez les activités qui seront confiées à·aux ingénieur·e·s (si possible, avec un planning de tâches attendues)
Décider en concertation comment réaliser la structure modulaire Réécrire l'appel à la bibliothèque de polyèdres pour permettre une structure modulaire Implémenter les DBMs, et s'assurer de leur utilisation automatiquement pour les modèles compatibles (automates temporisés classiques) En option : implémenter les DBM paramétrées comme alternative aux polyèdres lorsque c'est possible
Commentaires
Mettre à jour