A Formal Model for CARE Usability Properties Verification in Multimodal HCI

This paper proposes a generic, operational and formal model allowing to represent on the one hand the input multimodal user interaction task and on the other hand the CARE usability properties (complementarity, assignation, redundancy and equivalence). Each property is described by a transition system corresponding to a user task model satisfying the property in consideration. To validate our model we use the model-checking technique. Once the multimodal interaction task model is designed, the corresponding property is checked using the SMV model-checker. For this, complementarity, assignation and equivalence properties are expressed in the CTL temporal logic and applied using the SMV model-checker. The redundancy property is validated using refinement and proof techniques.