Modélisation formelle d'IHM multimodales en sortie avec B Événementiel: Approche par généralisation et instanciation

摘要

Multimodal human-computer interfaces allow to return to the user, the information generated by the functional core by combining semantically several modalities. In order to design such interfaces for critical systems, we proposed a formal design model composed of two models: the semantic fission model and the allocation model. We have also developed a detailed Event B formalization for these two models, it is based on a generic approach by successive refinements, using four generic parameterized models combined to instantiation mechanisms that allows the formalization of concrete interfaces. This article is dedicated to the presentation of this Event B formalization, it describes the generic Event B development approach.%Les interfaces homme-machine multimodales en sortie permettent de restituer à l'utilisateur, l'information produite par le noyau fonctionnel en combinant sémantiquement plusieurs modalités. Dans l'optique de concevoir de telles interfaces pour des systèmes critiques, nous avons proposé un modèle formel de conception qui se décompose en deux modèles : le modèle de fission sémantique et le modèle d'allocation. Nous avons également développé une formalisation B Événementiel détaillée de ces deux modèles, elle repose sur une démarche générique par raffinements successifs articulée autour de quatre modèles génériques paramétrés, accompagnés de mécanismes d'instanciation permettant l'utilisation des modèles génériques pour la formalisation d'interfaces concrètes. Cet article est dédié à la présentation de cette formalisation B Événementiel, il décrit la démarche générale de développement B Événementiel.