3 séminaires et soutenance HDR de Mohamed Tahar BHIRI : "Contributions pour la coopération entre démarches, modèles et outils formels et semi-formels"

Michael LEUSCHEL : "La programmation par contraintes en B"
Le discours va examiner l’utilité de la programmation par contraintes pour la validation de modèles formels, en particulier de modèles B.
On va aussi examiner la possibilité d’exprimer des problèmes à contraintes en B et d’utiliser ProB pour résoudre ces problèmes.
Des applications pratiques, par exemple pour la validation de données, vont être présentées.
(Le discours sera en français et les transparents en anglais).

Jean-Claude ROYER  : "Un langage abstrait pour la responsabilisation : spécification et contrôles"
Dans cet exposé je ferai une synthèse des travaux que nous avons faits sur la notion de responsabilité ("accountability'') dans le cadre de l'IP A4Cloud (http://www.a4cloud.eu/). La sécurité classique, bien qu'ayant fait des progrès, souffre encore de nombreuses faiblesses. Une raison essentielle est qu'elle est préventive et parfois trop stricte.
La "reponsabilisation" vise à mettre en oeuvre l'idée que la punition peut-être dissuasive et donc un mécanisme de contrôle a posteriori de l'historique d'un système. Je présenterai un langage abstrait pour la reponsabilisation avec une sémantique translationnelle vers la logique linéaire du premier ordre. Je montrerai que ce cadre offre un certain confort d'expression et un avantage certain en permettant des vérifications automatiques (conflict, compliance, propriétés). Nous aborderons également la problématique du monitoring de ces propriétés. Un prototype, AccLab, a été implémenté et est disponible à http://web.emn.fr/x-info/acclab/.

Mohamed Tahar Bhiri - habilitation à diriger des recherches : 
« Contributions pour la coopération entre démarches, modèles et outils formels et semi-formels »
Le jury composé de :
                   Monsieur Yves LEDRU, Professeur à l'Université Grenoble Alpes, Président
                   Madame Régine LALEAU, Professeur à l'Université Paris-Est Créteil, Rapporteur
                   Monsieur Michael LEUSCHEL, Professeur à l'Université Düsseldorf, Rapporteur
                   Monsieur Jean-Claude ROYER, Professeur à l'École des Mines de Nantes, Rapporteur
                   Monsieur Jean-Pierre GIRAUDIN, Professeur à l'Université Grenoble Alpes, Examinateur

L’obtention du logiciel de qualité demeure un défi pour la plupart des informaticiens. Le Génie Logiciel apporte divers moyens favorisant la qualité du logiciel. Ces moyens sont issus essentiellement de l’approche semi-formelle et formelle. Ce mémoire d’Habilitation apporte plusieurs contributions pour la coopération entre le semi-formel et formel. Pour y parvenir, nous avons touché à plusieurs domaines de recherche : objet, composant, architecture logicielle, raffinement, refactoring et aides méthodologiques pour le développement formel en Event-B. Ainsi, nous avons établi plusieurs démarches permettant : le passage d’une spécification formelle ADT vers UML/OCL, le passage d’Event-B vers UML/OCL, la vérification formelle d’assemblages de composants à base d’UML2.0, le raffinement avec preuve mathématique de modèles UML, le refactoring avec préservation du comportement de modèles UML, le développement formel des programmes séquentiels en Event-B, l’ouverture d’Event-B sur la planification en IA en passant par le langage formel PDDL et la décomposition des spécifications centralisées en Event-B. Egalement, nous avons proposé des outils d’ouverture d’UML2.0sur les langages formels (Acme/Armani, Wright et CSP de Hoare) et un outil IDM de validation permettant l’exécution d’une architecture logicielle décrite initialement en UML2.0 en passant par Wright et Ada concurrent. De plus, nous avons augmenté la bibliothèque de classes d’OCL par des concepts mathématiques avancés (couple, relation et fonction). Enfin, nous avons développé des bibliothèques de classes de qualité dans divers domaines : Grafcet, OBDD et Compression des programmes Bytecode Java.

Mots-clés : Coopération entre le semi-formel et formel, Objet, Composant, Architecture Logicielle, Raffinement, Refactoring

                   La soutenance sera suivie d’un pot auquel vous êtes également convié.

Régine LALEAU : "Modéliser le domaine pour enrichir le modèle de buts SysML/KAOS"
L'une des difficultés majeures liées à l'utilisation des méthodes formelles est l'élaboration d'une première spécification formelle à partir d'un cahier des charges issu de la phase d'analyse des exigences.
Nous proposons d'utiliser une approche de conception dans laquelle un modèle initial Event-B est construit à partir d'un modèle des exigences exprimé en SysML/KAOS, une extension de SysML avec des concepts de KAOS, une méthode d'ingénierie des exigences orientée buts. Le modèle des buts est complété par un modèle de domaine qui permet de capturer la connaissance liée à la structure des applications. Ce modèle de domaine est spécifié par une ontologie et un diagramme de classes.