A model-checking approach for the verification of CARE usability properties for multimodal user interfaces

dc.contributor.author Kamel, Nadjet
dc.contributor.author Selouani, Sid-Ahmed
dc.contributor.author Hamam, Habib
dc.date.accessioned 2020-04-28T09:18:13Z
dc.date.available 2020-04-28T09:18:13Z
dc.date.copyright 2009
dc.date.issued 2009-01
dc.description This 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_Interfaces en_US
dc.description.abstract A 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. en_US
dc.identifier.citation Kamel, 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. en_US
dc.identifier.issn 18286003
dc.identifier.uri 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_Interfaces
dc.identifier.uri http://hdl.handle.net/20.500.12519/211
dc.language.iso en en_US
dc.publisher Praise Worthy Prize S.r.l. en_US
dc.relation Authors Affiliations : Kamel, N., University of Moncton, Shippagan Campus 218, Boul. J.D. Gauthier, Shippagan, NB, E8S2K1, Canada; Selouani, S.A., University of Moncton, Shippagan Campus 218, Boul. J.D. Gauthier, Shippagan, NB, E8S2K1, Canada; Hamam, H., Université of Moncton and Canadian University of Dubai, Moncton, NB, E1A3E9, Canada
dc.relation.ispartofseries International Review on Computers and Software;Vol. 4, no. 1
dc.rights Permission to reuse abstract has been secured from Praise Worthy Prize S.r.l.
dc.rights.holder Copyright : 2009 Praise Worthy Prize S.r.l. - All rights reserved.
dc.subject Mobile cell phones en_US
dc.subject Model checke en_US
dc.subject Model-checking techniques en_US
dc.subject Multimodal user interfaces en_US
dc.subject Reachability en_US
dc.subject Symbolic model verifiers en_US
dc.subject Temporal logic formula en_US
dc.subject Transition systems en_US
dc.subject Usability properties en_US
dc.subject Cell membranes en_US
dc.subject Formal methods en_US
dc.subject Telecommunication equipment en_US
dc.subject Temporal logic en_US
dc.subject User interfaces en_US
dc.subject Model checking en_US
dc.title A model-checking approach for the verification of CARE usability properties for multimodal user interfaces en_US
dc.type Article en_US
Files
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
2.23 KB
Format:
Item-specific license agreed upon to submission
Description: