Kamel, NadjetSelouani, Sid-AhmedHamam, Habib2020-01-302020-01-3020082008Kamel, N., Selouani, S. A., Hamam, H. (2008). A modal logic for the CARE usability properties for multimodal user interfaces. In Proceedings of the 2008 International Conference on Software Engineering Research and Practice, SERP 2008 (pp. 39–45).1601320884;9781601320889http://www.ndsl.kr/ndsl/search/detail/article/articleSearchResultDetail.do?cn=NPAP08270949http://hdl.handle.net/20.500.12519/97This conference paper is not available at CUD collection. The version of scholarly record of this conference paper is published in SERP 2008 : proceedings of the 2008 International Conference on Software Engineering Research & Practice (2008), available online at: http://www.ndsl.kr/ndsl/search/detail/article/articleSearchResultDetail.do?cn=NPAP08270949This 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.enPermission to reuse abstract has been secured from CSREA Press .Axiom systemsCare usability propertiesLogicsModal logicModel-checking techniquesMulti modalsMulti-modal interactionsMultimodal user interfacesSatisfiabilityTransition systemsTravel information systemsEngineering researchInformation theoryInteractive computer systemsModel checkingSoftware engineeringSpecificationsUser interfacesConference PaperCopyright : 2008 CSREA Press