Browsing by Author "Kamel, Nadjet"
Now showing 1 - 2 of 2
Results Per Page
Sort Options
Item A modal logic for the CARE usability properties for multimodal user interfaces(2008) Kamel, Nadjet; Selouani, Sid-Ahmed; Hamam, HabibThis paper proposes the use of model- checking technique to validate Multimodal User Interfaces (MUIs). It introduces a modal logic to express the CARE (Complementarity, Assignation, Redundancy and Equivalent) usability properties for MUIs : the LCARE modal logic. The syntax, the semantics and an axiom system for LCARE are defined. LCARE allows for the specification of the CARE usability properties that a MUI must satisfy. The model-checking technique is used to check whether a CARE property, expressed in LCARE, is satisfied by a MUI. For this purpose the user multimodal interactions are modeled by a transition system and the CARE properties are expressed in LCARE formulae. A satisfiability relation is defined. It checks whether a LCARE formula is satisfied by the transition system modeling the multimodal interactions. LCARE allows for the specification of all the CARE usability properties. An illustration is given for the Matis application (Multimodal Airline Travel Information System) as a case study.Item A model-checking approach for the verification of CARE usability properties for multimodal user interfaces(Praise Worthy Prize S.r.l., 2009-01) Kamel, Nadjet; Selouani, Sid-Ahmed; Hamam, HabibA model-checking-based approach is proposed to verify the CARE (Complementarity, Assignement, Redundancy and Equivalence) usability properties for Multimodal User Interfaces (MUIs). This approach reduces the states explosion problem which is the main inconvenience of the model-checking technique. For this, we propose to decompose the transition system describing the behaviours of the MUI into a set of transition systems, and we decompose the temporal logic formula, that specifies the CARE property, into a set of reachability property formulas. The decomposition is based on disabling a set of modalities in the system. The model-checking process of the CARE property is done through a set of stages. At each stage a reachability formula is checked on a MUI component transition system. The process is aborted if a reachability formula is not satisfied. This approach reduces the complexity of the CARE model-checking process. We illustrate this approach, using the SMV (Symbolic Model Verifier) model-checker, on a MUI of a mobile cell phone case study. © 2009 Praise Worthy Prize S.r.l. - All rights reserved.