A Formal model to handle the adaptability of Multimodal User Interfaces

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.