Browsing by Author "Ait Ameur, Yamine"

Now showing 1 - 4 of 4
  • Thumbnail Image
    Item
    A formal model for output multimodal HCI
    (Springer Vienna, 2015-07) Mohand Oussaïd, Linda; Ait Sadoune, Idir; Ait Ameur, Yamine; Ahmed-Nacer, Mohamed
    Multimodal human–computer interaction (HCI) combine modalities at an abstract specification level in order to get information from the user (input multimodality) and to return information to the user (output multimodality). These multimodal interfaces use two mechanisms: first, the fusion of information transmitted by the user on different modalities during input interaction and second, the fission or decomposition of information produced by the functional core in order to distribute the composite information on the different modalities during output interaction. In this paper, we present a generic approach to design output multimodal interfaces. This approach is based on a formal model, composed of two models: semantic fission model for information decomposition process and allocation model for modalities and media allocation to composite information. An Event-B formalization has been proposed for the fission model and for allocation model. This Event-B formalization extends the generic model and support the verification of some relevant properties such as safety or liveness. An example of collision freeness property verification is presented in this paper.
  • Thumbnail Image
    Item
    A generic formal model for fission of modalities in output multi-modal interactive systems
    (2009) Mohand Oussaïd, Linda; Ait Ameur, Yamine; Ahmed-Nacer, Mohamed
    Output multi-modal human-machine interfaces combine semantically output medias and modalities in order to increase interaction machine capabilities. The aim of this paper is to present a formal model supporting formal specifications of output multi-modal interactive systems. As a consequence, the expected usability and robustness properties can be expressed and checked. This paper proposes a generic model which permits to specify the output multimodal interfaces following the CASE design space.
  • Thumbnail Image
    Item
    Formal modelling of output multi-modal HCI in Event-B. Modalities and media allocation
    (CERIST, 2013-12-15) Mohand Oussaïd, Linda; Ait Sadoune, Idir; Ait Ameur, Yamine
    Multi-modal Human-Computer Interfaces (HCI) allow interface designers to combine interactive modalities in order to increase interactive systems robustness and usability. In particular, output multi-modal interfaces allow the system to return the information to the user by using several modalities and media. In order to design such interfaces for critical systems, we proposed a generic formal model for the design of output multimodal interfaces. The proposed model consists of two successive models: the fission model that describes the semantic decomposition of information produced by the functional core into elementary information, and the allocation model that specifies the allocation of pairs modality/media for each elementary information. In a previous work (Mohand-Oussaid, Ait-Sadoune, and Ait-Ameur 2011), we have proposed an Event-B implementation of the fission model. In this paper, we present an Event-B implementation of the allocation model.
  • Thumbnail Image
    Item
    modélisation formelle d'IHM multi-modales en sortie avec B Evénementiel
    (CERIST, 23-04-2014) Mohand Oussaïd, Linda; Ait Sadoune, Idir; Ait Ameur, Yamine; Ahmed-Nacer, Mohamed
    Les interfaces homme-machine (IHM) multi-modales offrent à l’utilisateur la possibilité de combiner les modalités d’interaction afin d’augmenter la robustesse et l’utilisabilité de l’interface utilisateur d’un système. Plus particulièrement, en sortie, les IHM multi-modales permettent au système 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 des interfaces multi-modales en sortie. Le modèle proposé se décompose en deux modèles : le modèle de fission sémantique qui décrit la décomposition de l’information à restituer en informations élémentaires, et le modèle d’allocation qui spécifie l’allocation des modalités et médias aux informations élémentaires. Nous avons également développé une formalisation B Événementiel détaillée des deux modèles : fission sémantique et allocation. Cet article est dédié à la présentation d’une démarche formelle et générique relative au modèle proposé, il décrit la démarche générale de développement B Événementiel ainsi que le modèle générique B Événementiel correspondant au modèle de conception générique.