1st International ICST Conference on Ambient Media and Systems

Research Article

A Formal model to handle the adaptability of Multimodal User Interfaces

Download414 downloads
  • @INPROCEEDINGS{10.4108/ICST.AMBISYS2008.2882,
        author={Nadjet KAMEL and Yamine AIT AMEUR and Sid-Ahmed SELOUANI and Habib HAMAM},
        title={A Formal model to handle the adaptability of Multimodal User Interfaces},
        proceedings={1st International ICST Conference on Ambient Media and Systems},
        publisher={ICST},
        proceedings_a={AMBI-SYS},
        year={2010},
        month={5},
        keywords={multimodal interaction formal model adaptability},
        doi={10.4108/ICST.AMBISYS2008.2882}
    }
    
  • Nadjet KAMEL
    Yamine AIT AMEUR
    Sid-Ahmed SELOUANI
    Habib HAMAM
    Year: 2010
    A Formal model to handle the adaptability of Multimodal User Interfaces
    AMBI-SYS
    ICST
    DOI: 10.4108/ICST.AMBISYS2008.2882
Nadjet KAMEL1,*, Yamine AIT AMEUR2,*, Sid-Ahmed SELOUANI1,*, Habib HAMAM3,*
  • 1: Université de Moncton, Campus de Shippagan, N.-B. Canada
  • 2: LISI/ENSMA, BP 40109, 86961 Fururoscope Cedex, France
  • 3: Université de Moncton and Canadian University of Dubai Campus de Moncton N.-B. Canada
*Contact email: nadjet@umcs.ca, yamine@ensma.fr, selouani@umcs.ca, hamamh@umoncton.ca

Abstract

In this paper we propose an approach for checking adaptabil- ity property of multimodal User Interfaces (UIs) for systems used in dynamic environments like mobile phones and PDAs. The approach is based on a formal description of both the multimodal interaction and the property. The SMV model- checking formal technique is used for the verification process of the property. The approach is defined in two steps. First, the system is described using a formal model, and the prop- erty is specified using CTL (Computation Tree Logic) tem- poral logic. Then, we assume that an environment changes such that at most one modality of the system is disabled. For this propose, Disable is defined as a formal operator that disables a modality in the system. The property is checked by using the SMV (Symbolic Model Verifier) model-checker on all systems resulting from desabling a modality of the system. The approach reduces the complexity of the model- checking process and allows the verification at earlier stages of the development life cycle. We apply this approach on a mobile phone case study.