Mohand Oussaïd, LindaAit Sadoune, IdirAit Ameur, Yamine2013-12-152013-12-152013-12-15http://dl.cerist.dz/handle/CERIST/493Multi-modal Human-Computer Interfaces (HCI) allow interface designers to combine interactive modalities in order to increase interactive systems robustness and usability. In particular, output multi-modal interfaces allow the system to return the information to the user by using several modalities and media. In order to design such interfaces for critical systems, we proposed a generic formal model for the design of output multimodal interfaces. The proposed model consists of two successive models: the fission model that describes the semantic decomposition of information produced by the functional core into elementary information, and the allocation model that specifies the allocation of pairs modality/media for each elementary information. In a previous work (Mohand-Oussaid, Ait-Sadoune, and Ait-Ameur 2011), we have proposed an Event-B implementation of the fission model. In this paper, we present an Event-B implementation of the allocation model.Multi-modal interactionModalitiesMediaformal designformal verificationTechnical ReportCERIST-DSISM/RR--13-000000030--dz