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

Simple item page
dc.contributor.authorKamel, Nadjet
dc.contributor.authorSelouani, Sid-Ahmed
dc.contributor.authorHamam, Habib
dc.date.accessioned2020-04-28T09:18:13Z
dc.date.available2020-04-28T09:18:13Z
dc.date.copyright2009
dc.date.issued2009-01
dc.descriptionThis 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_Interfacesen_US
dc.description.abstractA 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.citationKamel, 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.issn18286003
dc.identifier.urihttps://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.urihttp://hdl.handle.net/20.500.12519/211
dc.language.isoenen_US
dc.publisherPraise Worthy Prize S.r.l.en_US
dc.relationAuthors 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.ispartofseriesInternational Review on Computers and Software;Vol. 4, no. 1
dc.rightsPermission to reuse abstract has been secured from Praise Worthy Prize S.r.l.
dc.rights.holderCopyright : 2009 Praise Worthy Prize S.r.l. - All rights reserved.
dc.subjectMobile cell phonesen_US
dc.subjectModel checkeen_US
dc.subjectModel-checking techniquesen_US
dc.subjectMultimodal user interfacesen_US
dc.subjectReachabilityen_US
dc.subjectSymbolic model verifiersen_US
dc.subjectTemporal logic formulaen_US
dc.subjectTransition systemsen_US
dc.subjectUsability propertiesen_US
dc.subjectCell membranesen_US
dc.subjectFormal methodsen_US
dc.subjectTelecommunication equipmenten_US
dc.subjectTemporal logicen_US
dc.subjectUser interfacesen_US
dc.subjectModel checkingen_US
dc.titleA model-checking approach for the verification of CARE usability properties for multimodal user interfacesen_US
dc.typeArticleen_US

Files

Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
Access Instruction 211.pdf
Size:
105.28 KB
Format:
Adobe Portable Document Format
Description:
Download

Collections

Department of Computer Engineering and Computational Sciences