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 en utilisant des approches basées sur le raffinement et 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.

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.

One of the main benefits of SOA architecture is the ability to compose existing services to provide more complex functionality. This services composition process, especially Web services, is generally defined by a choreography or an orchestration of atomic services. These compositions are seen as state-transitions systems expressing the communication protocol between the participating services. Services Workflows description languages describing these compositions suffer from the lack of formal semantics and the presence of ambiguities in their constructor's definitions in standards defining these languages. The associated tools do not offer the possibility to formally verify and validate the behaviour and the obtained services' composition properties.
This thesis focuses on the modelling and formal verification of the Web services composition described with the BPEL standard using the Event-B method. The proposed approach models the static and dynamic parts of BPEL and is based on refinement for structuring the BPEL process development. The theorem-proving technique is used for setting properties. A one-to-one link is guaranteed between the BPEL elements and their Event-B corresponding. This correspondence assists developers in improving the BPEL process's quality. This approach has been implemented in the BPEL2B tool.

This work defines a formal approach allowing to animate Event-B models. Invariants and deadlock freeness properties are expressed and proved in these models. The proposed approach suggests completing the proof activity in the Event-B method by animation activity. The obtained animator may be used to check if the obtained Event-B models fulfil user requirements or to help the developer when describing its formal Event-B models, particularly in defining Event-B invariants and guards. More precisely, Event-B models are translated into data models expressed in the EXPRESS formal data modelling method. The obtained data models are instantiated and provide an animation of the original Event-B models. Following this approach, it becomes possible to trigger the events of Event-B models, which themselves trigger entity instantiation on the EXPRESS side. As a further step, we show that the Event-B models can be used as a monitoring system, raising alarms in case of incorrect systems behaviour. The proposed approach is operationally implemented in the B2EXPRESS tool, which handles the animation of Event-B models. It has experimented in the case of validating multimodal human interfaces in the context of the VERBATIM project.