LogoLogo

Djeddai, Selma. Combining formal verification environments and model-driven engineering

Djeddai, Selma (2013). Combining formal verification environments and model-driven engineering.

[img]PDF - nécessite un logiciel de visualisation PDF comme GSview, Xpdf or Adobe Acrobat Reader
1450Kb

Résumé en francais

Les méthodes formelles (comme les prouveurs interactifs) sont de plus en plus utilisées dans la vérification de logiciels critiques. Elles peuvent compter sur leurs bases formelles solides ainsi que sur leurs sémantiques précises. Cependant, elles utilisent des notations complexes qui sont souvent difficiles à comprendre. D'un autre côté, l'Ingénierie Dirigée par les Modèles nous propose des langages de descriptions, comme les diagrammes de classes, utilisant des notations intuitives mais qui souffrent d'un manque de bases formelles. Dans cette thèse, nous proposons de faire interagir les deux domaines complémentaires que sont les méthodes formelles et l'ingénierie dirigée par les modèles. Nous proposons une approche permettant de transformer des types de données fonctionnels (utilisés dans les prouveurs interactifs) en diagrammes de classes et vice-versa. Afin d'atteindre ce but, nous utilisons une méthode de transformation dirigée par les modèles.

Sous la direction du :
Directeur de thèse
Matthes, Ralph
Strecker, Martin
Ecole doctorale:Mathématiques, informatique, télécommunications de Toulouse (MITT)
laboratoire/Unité de recherche :Institut de Recherche en Informatique de Toulouse (IRIT), UMR 5505
Mots-clés libres :Transformation de modèles - Ingénierie Dirigée par les Modèles (IDM) - Méthodes formelles - Vérification
Sujets :Informatique
Déposé le :04 Nov 2013 10:57