logo EDITE Sujets de doctorat

Vérification formelle des diagrammes dynamiques UML2 : Applications aux systèmes Temps-Réels Embarqués.

Résumé rédigé par
Directeur de thèse:
Doctorant: Aymen LOUATI
Unité de recherche EA 1395 Centre d'Étude et de Recherche en Informatique et Communications

Projet

Le manque de sémantique du langage de modélisation UML (Unified Modeling langage) est souvent invoqué comme atout à la vulgarisation de la notation favorisant sa large utilisation, la correction de la modélisation requiert en revanche une sémantique formelle rigoureusement définie. Dans ce sens, UML2.0 apporte plus de précisions à UML1.x mais la notation reste informelle et manque d'outils pour l'analyse et la vérification automatique des modèles. Dans un premier temps, le travail de thèse devra commencer par l'étude détaillée de la sémantique des différents diagrammes dynamiques (diagrammes d’interactions (séquence, collaboration) diagramme d’activité, diagramme de cas d’utilisation) afin de bien cerner leurs insuffisances révélées lors de l'élaboration d'UML2.0 y compris les extensions proposées pour décrire les exigences temporelles. Dans un second temps, nous devrons proposer un ou plusieurs formalismes (basé sur les réseaux de Pétri temporisé ou autre) capables de doter les diagrammes UML d’une sémantique formelle permettant ainsi de mener une vérification aussi bien qualitative que quantitative. Enfin, nous chercherons à valider l'approche développée sur les systèmes Temps-Réels Embarqués, pour s'assurer de leur bon fonctionnement logique ou temporel à travers une application significative.