Kamel, NadjetSelouani, Sid-AhmedHamam, Habib2020-04-282020-04-2820092009-01Kamel, N., Selouani, S. A., & Hamam, H. (2009). A model-checking approach for the verification of CARE usability properties for multimodal user interfaces. International Review on Computers and Software, 4(1), 152–160.18286003https://www.praiseworthyprize.org/latest_issues/IRECOS-latest/IRECOS_vol_4_n_1.html#A_Model-Checking_Approach_for_the_Verification_of_CARE_Usability_Properties_for_Multimodal_User_Interfaceshttp://hdl.handle.net/20.500.12519/211This article is not available at CUD collection. The version of scholarly record of this Article is published in International Review on Computers and Software (2009), available online at: https://www.praiseworthyprize.org/latest_issues/IRECOS-latest/IRECOS_vol_4_n_1.html#A_Model-Checking_Approach_for_the_Verification_of_CARE_Usability_Properties_for_Multimodal_User_InterfacesA 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.enPermission to reuse abstract has been secured from Praise Worthy Prize S.r.l.Mobile cell phonesModel checkeModel-checking techniquesMultimodal user interfacesReachabilitySymbolic model verifiersTemporal logic formulaTransition systemsUsability propertiesCell membranesFormal methodsTelecommunication equipmentTemporal logicUser interfacesModel checkingA model-checking approach for the verification of CARE usability properties for multimodal user interfacesArticleCopyright : 2009 Praise Worthy Prize S.r.l. - All rights reserved.