Informations professionnelles
Statut: Docteur ED
ED: EDITE
Unité de recherche: LIP6
Employeur: Univ. Montpellier Date de debut de thèse: 1 janvier 2017 Date soutenance de thèse: 22 décembre 2021 Directeur de thèse: Pascal POIZAT (LIP6) Directeur de thèse: Souheib BAARIR (LRE) Sujet de thèse: Vérification paramétrée et dérivation de code à partir de spécifications formelles pour les systèmes embarqués Thématique : Modèles de calcul, preuve, vérification
Employeur: Univ. Montpellier Date de debut de thèse: 1 janvier 2017 Date soutenance de thèse: 22 décembre 2021 Directeur de thèse: Pascal POIZAT (LIP6) Directeur de thèse: Souheib BAARIR (LRE) Sujet de thèse: Vérification paramétrée et dérivation de code à partir de spécifications formelles pour les systèmes embarqués Thématique : Modèles de calcul, preuve, vérification
Soutenance de thèse
Données générales
Titre : Parameterized Verification from Formal Specifications of Information Systems
Date : 22 décembre 2021
Heure: 14:00
Résumé : La vérification des modèles de processus métiers est cruciale pour permettre d'y détecter d'éventuelles erreurs dès la conception, plutôt qu'à l'exécution sur des moteurs de processus métier. Dans cette thèse, Nous avons défini une approche pour la vérification de modèles de collaboration de processus métiers qui supporte plusieurs de ces perspectives, à savoir les différents modèles de communication et les contraintes liées au temps. Pour cela nous avons défini une sémantique d'exécution formelle, en termes de logique du premier ordre, au fragment de BPMN pris en compte. Nous avons ensuite défini des implantations de cette sémantique dans les langages formels TLA+ et Alloy. Ceci a, enfin, permis la vérification des modèles à l'aide des outils dédiés à ces langages formels. Notre approche est supportée par un outil, fbpmn, permettant les transformation formelles de modèles BPMN vers TLA+ et Alloy, la vérification des modèles, et l'animation de contre-exemples.
Lieu : Laboratoire d'Informatique Paris 6, Sorbonne Université.
Rapporteurs/ Rapporteuses
| Personne | Qualité | Etablissement |
|---|---|---|
| M. Salaün Gwen | Professeur des universités | Inria Grenoble - Rhône-Alpes |
| Mme. Re Barbara | Maîtresse de Conférences (HDR) | Processes and Services Lab, University of Camerino (Italie) |
Composition du jury
| Personne | Qualité | Etablissement |
|---|---|---|
| M. Poizat Pascal | Professeur des universités | LIP6, Univ. de Nanterre |
| M. Baarir Souheib | Maître de Conférences (HDR) | Laboratoire de Recherche de l'EPITA, Univ. de Nanterre |
| M. Kahloul Laïd | Professeur des universités | Laboratoire d’Informatique Intelligente, Université Mohamed Khider (Algérie) |
| Mme. Bérard Béatrice | Professeure des universités | LIP6, Sorbonne Université |
| Mme. Hamza Lamia | Maîtresse de Conférences | Laboratoire d’Informatique Médicale, Université Abderrahmane Mira (Algérie) |
| M. Tibermacine Okba | Maître de Conférences | Laboratoire de Recherche des Systèmes Experts, Ingénierie et leurs Applications dans l’ingénierie, Université Mohamed Khider (Algérie) |
| Mme. Re Barbara | Maîtresse de Conférences (HDR) | Processes and Services Lab, University of Camerino (Italie) |
| M. Salaün Gwen | Professeur des universités | Inria Grenoble - Rhône-Alpes |