RECHERCHE

Mes activités de recherche abordent le thème de l'utilisation des méthodes formelles
pour la modélisation et la vérification des systèmes.

Thèmes de recherche | Publications | Développements

THEMES DE RECHERCHE

Intégration des ontologies dans le développement de systèmes discrets fondés sur la preuve.

Plusieurs propriétés importantes sont vérifiées en méthode formelle. Elles sont définies et vérifiées à partir de la sémantique implicite associée à la technique formelle utilisée : contrôle de types, preuve, réécriture, raffinement, model checking, analyse de traces, simulation etc. Lorsque ces propriétés sont traitées dans leur contexte en leur associant une sémantique explicite, elles peuvent ne plus être valides. Un exemple est la composition de systèmes échangeant des flottants représentant des monnaies exprimées en dollars dans l'un et en euros dans l'autre. L'absence de sémantique explicite dans le contexte de preuve rend cette composition invalide. Ainsi, les activités de développement doivent être reconsidérées en fonction de la possibilité de représenter non seulement la sémantique implicite mais aussi la sémantique explicite. La formalisation de ces opérations de développement en séparant l'implicite de l'explicite renforcerait la correction des systèmes ainsi développés. Cet aspect constitue un problème significatif si l'on souhaite développer des systèmes dynamiques, à base de composants hétérogènes fiables, dans des contextes qui ne le sont pas.

Modélisation et Vérification de systèmes à base d’événements.

Dans nos travaux de recherche, nous nous sommes intéressés à l’étude des systèmes à base d'états et de transitions (événements) entre les états. La méthode Event-B a été utilisée pour implémenter notre démarche de modélisation et de vérification. Un modèle Event-B décrit un système d’états-transitions par un ensemble d’états et un ensemble d’événements. Les actions effectuées par les événements permettent la transition entre états. L’opération de raffinement est utilisée pour structurer le développement, et la preuve de théorèmes pour vérifier des propriétés sur ces systèmes.

Comme application de notre démarche, nous avons étudié les problématiques suivantes :
L’utilisabilité des IHM multimodales en entrée.
Restitution de l’information et allocation des présentations multimodales dans les IHM multimodales en sortie.
Vérification des propriétés comportementales et fonctionnelles d'une orchestration de services.
Vérification des propriétés transactionnelles d'une composition de services.

Animation de modèles.

Ce travail présente une démarche outillée permettant d’animer et de tester des modèles Event-B. Notre approche définit une transformation d’un modèle Event-B en un modèle à objets, représentant un système d’événements, exprimé dans le langage de modélisation de données EXPRESS. Le modèle (ou le schéma) obtenu peut être instancié pour déclencher des événements particuliers du modèle Event-B traduit. Une expression d’algèbre de processus exprimant un scénario décrivant une trace d’événements Event-B guide l’animation de ces modèles événementiels. L’outil résultant, dénommé B2EXPRESS, est utilisé dans le but de contrôler si des scénarios correspondent à une utilisation licite ou non du système d’événements décrits avec Event-B. B2EXPRESS permet également d’animer ces modèles selon plusieurs modes, permettant de détecter des blocages ou bien des invariants non satisfaits. Il assiste le développeur dans la preuve des obligations de preuve générées. Les erreurs détectées sont localisées dans le modèle Event-B animé.

Cliquez ici pour revenir en haut de la page

DERNIERES PUBLICATIONS

Cliquez ici pour accèder à la liste complète des publications

Building Formal Semantic Domain Model: An Event-B Based Approach
9th International Conference on Model and Data Engineering

The role of user requirements in data repository design
International Journal on Software Tools for Technology Transfer

Formal Modelling of Ontologies : An Event-B based Approach Using the Rodin Platform
Electronic Proceedings in Theoretical Computer Science

Using the Isabelle Ontology Framework. Linking the Formal with the Informal
11th International Conference on Intelligent Computer Mathematics

Cliquez ici pour revenir en haut de la page

DEVELOPPEMENTS

OntoEventB Rodin plugin

Page Web du plugin

OntoEventB implémentant une approche de formalisation des ontologies décrites par des langages de description des ontologiques (OWL, OntoML, ...) en utilisant la théorie des ensembles et la logique du premier ordre supportées par la méthode Event-B. L’intérêt de cette formalisation est d’enrichir le processus de spécification et de vérification utilisant la méthode Event-B, en intégrant des modèles de données et de connaissances décrits dans des ontologies. L’utilisation des ontologies dans un développement Event-B va servir à annoter et/ou à typer les données manipulées par le système, ce qui permet de vérifier, en plus des propriétés caractéristiques du système, des propriétés liées à la cohérence des données manipulées et induites par les contraintes du domaine exprimées dans les ontologies

BPEL2B Rodin plugin

Update site : https://wdi.supelec.fr/aitsadoune/bpel2b-update-site/

Le processus de composition de services Web est défini par une chorégraphie ou une orchestration de ces services. Les langages de description de la chorégraphie ou d’orchestration sont généralement décrits d’une manière informelle dans les spécifications et les outils associés n’offrent pas la possibilité de vérifier et de valider formellement le comportement et les propriétés du service composé obtenu. Dans nos travaux, on s’intéresse à la vérification formelle de l’orchestration de services décrite avec le langage BPEL en utilisant la méthode Event-B. L’approche proposée se base sur le raffinement pour la structuration du développement d’un processus BPEL, et sur la preuve de théorèmes pour l’établissement de propriétés. Le plugin BPEL2B implémente l’approche proposée.

CO2EB Rodin plugin

Update site : https://wdi.supelec.fr/aitsadoune/co4eb-update-site/

Our approach of modelling composition operations of a process algebra in Event-B follows the formal modelling rules formally defined in this paper. We propose to encode these operators in Event-B, using an explicit variant to encode the events order and successive refinements. Each process algebra expression defined by the rule A_0 ::= A_1 OP A_2 is modelled by two Event-B models. The first one is associated with the left hand side of the rule and contains only one event evt_A0 associated with the action A_0 . The second model is a refinement of the first one and corresponds to the right hand side of this rule. Two new events evt_A1 and evt_A2 associated with the actions A_1 and A_2 are added in the refinement. These events carry the semantics of the OP operator and of the right hand side of the expression. The firing order of the events is determined by introducing an explicit decreasing variant. The new events are fired and when they are completed, the refined event evt_A0 is fired.

B2EXPRESS Event-B Animator

Update site : (unavailable)

L’outil B2EXPRESS est un animateur de modèles Event-B fondé sur l’instanciation de modèles de données exprimés dans le langage EXPRESS. Chaque construction de modèle Event-B (substitutions, invariant, ensembles, variables, etc) est transformée en une construction de modèle EXPRESS (entité, attribut, regèles locales et globales). L’animation consiste à définir des instances des différentes entités du modèle EXPRESS obtenu et à contrôler les contraintes associées.

Cliquez ici pour revenir en haut de la page

Designed by Idir AIT SADOUNE