Combinaison de méthodes formelles pour la spécification de systèmes industriels

Description :
Conférencier : Thomas Fayolle

Résumé : La spécification d’un système industriel nécessite la collaboration d’un ingénieur connaissant le système à modéliser et d’un ingénieur connaissant le langage de modélisation. L'utilisation d'un langage de spécification graphique, tel que les ASTD (Algebraic State Transition Diagram), permet de faciliter cette collaboration. Dans cette thèse, nous définissons une méthode de spécification graphique et formelle qui combine les ASTD avec les langages Event-B et B. L’ordonnancement des actions de la spécification est décrit par les ASTD et le modèle de données est décrit dans la spécification Event-B. La spécification B permet de vérifier la cohérence du modèle : les événements Event-B doivent pouvoir être exécutés lorsque les transitions associées doivent l’être. Un raffinement combiné des ASTD et d’Event-B permet la spécification incrémentale du système. Afin de valider son apport, la méthode de spécification a été utilisée pour la spécification de cas d’études.

Membre du jury, président rapporteur : Dominique Mery, professeur, Université de Lorraine
Membre du jury, président rapporteur : David Delahaye, professeur, Université de Montpellier
Membre du jury, directrice de recherche : Régine Laleau, professeure, Université Paris-Est Créteil
Membre du jury, codirecteur de recherche : Marc Frappier, professeur, Université de Sherbrooke
Membre du jury, évaluateur : Frédéric Gervais, Université Paris-Est Créteil
Membre du jury, évaluatrice : Catherine Dubois, professeure, École nationale d’informatique pour l’industrie et l’entreprise
Membre du jury, évaluatrice : Aïda Ouangraoua, professeure, Université de Sherbrooke
Membre du jury, évaluatrice : Amel Mammar, maître de conférences, Télécom Sud-Paris

Toutes les personnes intéressées sont cordialement invitées.