Une méthode inverse pour la synthèse de paramètres temporels dans les systèmes concurrents.
Mercredi 8 décembre 2010 à 14h30 à Cachan.
Salle de Conférences, Pavillon des Jardins,
École Normale Supérieure de Cachan.
Voir le plan d'accès au campus, et le plan du campus (le pavillon des jardins est le batiment numéro 5).
| Eugene Asarin | Président du jury |
| Bernard Berthomieu | Rapporteur |
| Franck Cassez | Rapporteur |
| Emmanuelle Encrenaz-Tiphene | Directrice de thèse |
| Laurent Fribourg | Directeur de thèse |
| Marta Kwiatkowska | Examinatrice |
| Kim G. Larsen | Examinateur |
Cette thèse propose une nouvelle approche pour la synthèse de valeurs temporelles dans les systèmes temporisés. Lorsque l'on vérifie un système temps-réel, comme un circuit ou un protocole de communication, il est important de vérifier non seulement l'aspect fonctionnel, mais également temporisé. La correction du système dépend de valeurs temporelles internes et de l'environnement. Les méthodes formelles de vérification garantissent la correction d'un système temporisé pour un ensemble de valeurs temporelles, mais ne donnent pas d'information pour d'autres valeurs. Vérifier la correction d'un système pour de nombreuses valeurs peut s'avérer long et difficile. Il est alors intéressant de les considérer comme paramètres. Le problème consiste alors à synthétiser des valeurs de ces paramètres pour lesquelles le système est correct. Nous nous intéressons ici à la synthèse de paramètres dans le cadre des automates temporisés. Notre approche est basée sur la méthode inverse suivante : à partir d'une instance de référence des paramètres, nous synthétisons une contrainte sur les paramètres, garantissant le même comportement que pour l'instance de référence, abstraction faite du temps. Il en résulte un critère de robustesse pour le système. En itérant cette méthode sur des points dans un domaine paramétrique borné, nous sommes alors à même de partitionner l'espace des paramètres en bonnes et mauvaises zones par rapport à une propriété à vérifier. Ceci nous donne une cartographie comportementale du système. Cette méthode s'étend aisément aux systèmes probabilistes. Nous présentons également des variantes de la méthode inverse pour les graphes orientés valués et les processus de décision markoviens. Parmi les prototypes implémentés, IMITATOR II implémente la méthode inverse et la cartographie pour les automates temporisés. Ce prototype nous a permis de synthétiser de bonnes valeurs pour les paramètres temporels de plusieurs études de cas, dont un modèle abstrait d'une mémoire commercialisée par le fabricant de puces ST-Microelectronics, ainsi que plusieurs protocoles de communication.
Mots-clés: vérification, model-checking, systèmes temporisés, automates temporisés paramétrés, synthèse de paramètres, vérification de circuits, automates temporisés probabilistes, protocoles de communication.
La version finale peut être visualisée ici.
Les diapositives de ma soutenance sont disponibles ici.
Voir aussi :