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 :