{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,14]],"date-time":"2023-01-14T14:29:28Z","timestamp":1673706568396},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"7","license":[{"start":{"date-parts":[[2015,6,10]],"date-time":"2015-06-10T00:00:00Z","timestamp":1433894400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Computing"],"published-print":{"date-parts":[[2015,7]]},"DOI":"10.1007\/s00607-015-0460-y","type":"journal-article","created":{"date-parts":[[2015,6,10]],"date-time":"2015-06-10T16:13:22Z","timestamp":1433952802000},"page":"713-740","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["A formal model for output multimodal HCI"],"prefix":"10.1007","volume":"97","author":[{"given":"Linda","family":"Mohand-Oussaid","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Idir","family":"Ait-Sadoune","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yamine","family":"Ait-Ameur","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mohamed","family":"Ahmed-Nacer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,6,10]]},"reference":[{"key":"460_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-book: assigning programs to meanings","author":"JR Abrial","year":"1996","unstructured":"Abrial JR (1996) The B-book: assigning programs to meanings. Cambridge University Press, New York"},{"key":"460_CR2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: system and software engineering","author":"JR Abrial","year":"2010","unstructured":"Abrial JR (2010) Modeling in Event-B: system and software engineering. Cambridge University Press, New York"},{"key":"460_CR3","unstructured":"Ait-Ameur Y, Ait-Sadoune I, Baron M (2006a) Etude et comparaison de sc\u00e9narios de d\u00e9veloppements formels d\u2019interfaces multi-modales fond\u00e9s sur la preuve et le raffinement. In: MOSIM 2006, 6\u00e8me Conf\u00e9rence Francophone de Mod\u00e9lisation et Simulation. Mod\u00e9lisation, Optimisation et Simulation des Syst\u00e8mes: D\u00e9fis et Opportunit\u00e9s, Rabat"},{"key":"460_CR4","doi-asserted-by":"crossref","unstructured":"Ait-Ameur Y, Ait-Sadoune I, Mota JM, Baron M (2006b) Validation et v\u00e9rification formelles de syst\u00e8mes interactifs multi-modaux fond\u00e9es sur la preuve. In: Proceedings of the 18th International Conference of the Association Francophone d\u2019Interaction Homme-Machine. ACM, Montr\u00e9al, pp 123\u2013130","DOI":"10.1145\/1132736.1132752"},{"issue":"3","key":"460_CR5","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1007\/s10009-009-0109-2","volume":"11","author":"Y Ait-Ameur","year":"2009","unstructured":"Ait-Ameur Y, Baron M, Kamel N, Mota JM (2009) Encoding a process algebra using the Event B method: application to the validation of human computer interactions. Int J Softw Tools Technol Transf 11(3):239\u2013253","journal-title":"Int J Softw Tools Technol Transf"},{"key":"460_CR6","unstructured":"Ait-Ameur Y, Ait-Sadoune I, Baron M, Mota JM (2010) V\u00e9rification et validation formelles de syst\u00e8mes interactifs fond\u00e9es sur la preuve : application aux syst\u00e8mes multi-modaux. Journal d\u2019Interaction Personne-Syst\u00e8me 1(1):1\u201330. http:\/\/www.journal-interaction-personne-systeme.fr\/articles\/80-articles\/85-vol-1-2010-num-1-art-3"},{"issue":"4","key":"460_CR7","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1016\/0953-5438(94)90008-6","volume":"6","author":"O Bernsen","year":"1994","unstructured":"Bernsen O (1994) Foundations of multimodal representations. A taxonomy of representational modalities. Interact Comput 6(4):347\u2013371","journal-title":"Interact Comput"},{"issue":"4","key":"460_CR8","doi-asserted-by":"crossref","first-page":"477","DOI":"10.1016\/S0920-5489(97)00013-5","volume":"6","author":"M Bordegoni","year":"1997","unstructured":"Bordegoni M, Faconti G, Maybury M, Rist T, Ruggieri S, Trahanias P, Wilson M (1997) A standard reference model for intelligent multimedia presentation systems. Comput Stand Interface 6(4):477\u2013496","journal-title":"Comput Stand Interface"},{"key":"460_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1007\/978-3-540-92698-6_3","volume-title":"Engineering Interactive Systems","author":"J Bouchet","year":"2008","unstructured":"Bouchet J, Madani L, Nigay L, Oriat C, Parissis I (2008) Formal testing of multimodal interactive systems. In: Gulliksen J, Harning M, Palanque P, van der Veer G, Wesson J (eds) Engineering Interactive Systems, vol 4940., Lecture Notes in Computer ScienceSpringer, Berlin Heidelberg, pp 36\u201352"},{"key":"460_CR10","series-title":"LNCS","first-page":"717","volume-title":"INTERACT","author":"ML Bourguet","year":"2003","unstructured":"Bourguet ML (2003) Designing and prototyping multimodal commands. INTERACT, vol 3., LNCSSpringer, Berlin, pp 717\u2013720"},{"key":"460_CR11","doi-asserted-by":"crossref","unstructured":"Cohen PR, Johnston M, McGee D, Oviatt S, Pittman J, Smith I, Chen L, Clow J (1997) Quickset: Multimodal interaction for distributed applications. In: Proceedings of the Fifth ACM International Conference on Multimedia, ACM, New York, MULTIMEDIA \u201997, pp 31\u201340","DOI":"10.1145\/266180.266328"},{"key":"460_CR12","first-page":"7","volume-title":"Actes de la Conf\u00e9rence IHM\u201994","author":"J Coutaz","year":"1994","unstructured":"Coutaz J, Nigay L (1994) Les propri\u00e9t\u00e9s CARE dans les interfaces multimodales. Actes de la Conf\u00e9rence IHM\u201994. Lille, France, pp 7\u201314"},{"key":"460_CR13","volume-title":"A discipline of programming","author":"EW Dijkstra","year":"1977","unstructured":"Dijkstra EW (1977) A discipline of programming, 1st edn. Prentice Hall PTR, Upper Saddle River","edition":"1"},{"key":"460_CR14","doi-asserted-by":"crossref","unstructured":"Duarte C, Carri\u00e7o L (2006) A conceptual framework for developing adaptive multimodal applications. In: Proceedings of the 11th international conference on Intelligent user interfaces. ACM, Sydney, pp 132\u2013139","DOI":"10.1145\/1111449.1111481"},{"key":"460_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/978-3-642-00437-7_1","volume-title":"Human Machine Interaction","author":"B Dumas","year":"2009","unstructured":"Dumas B, Lalanne D, Oviatt S (2009) Multimodal interfaces: a survey of principles, models and frameworks. In: Lalanne D, Kohlas J (eds) Human Machine Interaction, vol 5440., Lecture Notes in Computer ScienceSpringer, Berlin Heidelberg, pp 3\u201326"},{"key":"460_CR16","doi-asserted-by":"crossref","unstructured":"Flippo F, Krebs A, Marsic I (2003) A framework for rapid development of multimodal interfaces. In: Proceedings of the 5th International Conference on Multimodal Interfaces, ACM, New York, ICMI \u201903, pp 109\u2013116","DOI":"10.1145\/958432.958455"},{"key":"460_CR17","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1007\/1-4020-3304-4_28","volume-title":"Computer-aided design of user interfaces IV","author":"J Glass","year":"2005","unstructured":"Glass J, Weinstein E, Cyphers S, Polifroni J, Chung G, Nakano M (2005) A framework for developing conversational user interfaces. In: Jacob RJ, Limbourg Q, Vanderdonckt J (eds) Computer-aided design of user interfaces IV. Springer, Amsterdam, pp 349\u2013360"},{"key":"460_CR18","volume-title":"Design principles for interactive software","year":"1997","unstructured":"Gram C, Cockton G (eds) (1997) Design principles for interactive software. Chapman & Hall Ltd, London"},{"key":"460_CR19","unstructured":"Jourde F, Nigay L, Parissis I (2006) Test formel de syst\u00e8mes interactifs multimodaux : couplage ICARE - Lutess. In: ICSSEA\u20192006, 19\u00e8me journ\u00e9es Internationales \u201cg\u00e9nie logiciel & Ing\u00e9nierie de Syst\u00e8mes et leurs Applications\u201d Globalisation des services et des syst\u00e8mes, Paris"},{"key":"460_CR20","first-page":"219","volume-title":"16\u00e8me Conf\u00e9rence Francophone sur l\u2019Interaction Homme-Machine (IHM\u20192004)","author":"N Kamel","year":"2004","unstructured":"Kamel N (2004) Utilisation de SMV pour la v\u00e9rification de propri\u00e9t\u00e9s d\u2019IHM multimodales. 16\u00e8me Conf\u00e9rence Francophone sur l\u2019Interaction Homme-Machine (IHM\u20192004). ACM Press, Namur, Belgique, pp 219\u2013222"},{"key":"460_CR21","doi-asserted-by":"crossref","unstructured":"Kamel N, Ait-Ameur Y (2007) A formal model for CARE usability properties verification in multimodal HCI. In: IEEE International Conference on Pervasive Services. IEEE, Istanbul, pp 341\u2013348","DOI":"10.1109\/PERSER.2007.4283937"},{"key":"460_CR22","doi-asserted-by":"crossref","unstructured":"Krahnstoever N, Kettebekov S, Yeasin M, Sharma R (2002) A real-time framework for natural multimodal interaction with large screen displays. In: Proceedings of the 4th IEEE International Conference on Multimodal Interfaces, IEEE Computer Society, Washington, ICMI \u201902, p 349","DOI":"10.1109\/ICMI.2002.1167020"},{"key":"460_CR23","unstructured":"Larson JA, Raman T, Raggett D, Bodell M, Johnston M, Kumar S, Potter S, Waters K (2003) W3C multimodal interaction framework. W3C NOTE 6"},{"key":"460_CR24","unstructured":"MacColl I, Carrington D (1998) Testing MATIS: a case study on specification-based testing of interactive systems. In: Formal Aspects of Human Computer Interaction Workshop (FAHCI98), pp 57\u201369"},{"issue":"6","key":"460_CR25","doi-asserted-by":"crossref","first-page":"454","DOI":"10.1016\/j.jlap.2009.01.005","volume":"78","author":"L Madani","year":"2009","unstructured":"Madani L, Parissis I (2009) Automatically testing interactive applications using extended task trees. J Log Algebr Program 78(6):454\u2013471","journal-title":"J Log Algebr Program"},{"key":"460_CR26","doi-asserted-by":"crossref","unstructured":"Mohand-Oussaid L, Ait-Ameur Y, Ahmed-Nacer M (2009) A generic formal model for fission of modalities in output multi-modal interactive systems. In: International Workshop on Verification and Evaluation of Computer and Communication Systems, Rabat","DOI":"10.14236\/ewic\/VECOS2009.12"},{"key":"460_CR27","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/978-3-642-24443-8_22","volume-title":"MEDI: model and data engineering","author":"L Mohand-Oussaid","year":"2011","unstructured":"Mohand-Oussaid L, Ait-Sadoune I, Ait-Ameur Y (2011) Modelling information fission in output multi-modal interactive systems using Event-B. MEDI: model and data engineering. Springer, Obidos, pp 200\u2013213"},{"key":"460_CR28","unstructured":"Mohand-Oussaid L, Kamel N, Ait-Sadoune I, Ait-Ameur Y, Ahmed-Nacer M (2011) Human computer interaction in transport, ISTE Ltd and John Wiley and Sons Inc, chap A formal framework for design and validation of multimodal interactive systems in transport domain, pp 93\u2013108"},{"key":"460_CR29","doi-asserted-by":"crossref","unstructured":"Mohand-Oussaid L, Ait-Sadoune I, Ait-Ameur Y, Ahmed-Nacer M (2014) Formal modelling of output multi-modal HCI in Event-B: Modalities and media allocation. In: AAAI Symposium: modeling in human-machine systems: challenges for formal verification, Palo Alto","DOI":"10.1007\/s00607-015-0460-y"},{"key":"460_CR30","unstructured":"Mohand-Oussaid L, Ait-Sadoune I, Ait-Ameur Y, Ahmed-Nacer M (2014) Mod\u00e9lisation formelle d\u2019IHM multi-modales en sortie avec B \u00c9v\u00e9nementiel. In: Approches Formelles dans l\u2019Assistance au Dveloppement de Logiciels AFADL 2014, Paris, p 76"},{"key":"460_CR31","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4471-0043-0","volume-title":"Understanding formal methods","author":"JF Monin","year":"2003","unstructured":"Monin JF, Hinchey MG (2003) Understanding formal methods. Springer, New York"},{"key":"460_CR32","series-title":"LNCS","first-page":"25","volume-title":"INTERACT 2005","author":"D Navarre","year":"2005","unstructured":"Navarre D, Palanque P, Bastide R, Schyn A, Winckler M, Nedel L, Freitas C (2005) A formal description of multimodal interaction techniques for immersive virtual reality applications. INTERACT 2005., LNCSSpringer, Roma, pp 25\u201328"},{"key":"460_CR33","doi-asserted-by":"crossref","unstructured":"Nigay L, Coutaz J (1995) A generic platform for addressing the multimodal challenge. In: Proceedings of the SIGCHI Conference on Human Factors in Computing Systems, ACM Press\/Addison-Wesley Publishing Co., New York, CHI \u201995, pp 98\u2013105","DOI":"10.1145\/223904.223917"},{"issue":"4","key":"460_CR34","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1207\/S15327051HCI1504_1","volume":"15","author":"S Oviatt","year":"2000","unstructured":"Oviatt S, Cohen P, Wu L, Duncan L, Suhm B, Bers J, Holzman T, Winograd T, Landay J, Larson J et al (2000) Designing the user interface for multimodal speech and pen-based gesture applications: state-of-the-art systems and future research directions. Hum Comput Interact 15(4):263\u2013322","journal-title":"Hum Comput Interact"},{"key":"460_CR35","series-title":"LNCS","first-page":"03","volume-title":"INTERACT","author":"PA Palanque","year":"2003","unstructured":"Palanque PA, Schyn A (2003) A model-based approach for engineering multimodal interactive systems. INTERACT., LNCSSpringer, Berlin Heidelberg, pp 03\u201305"},{"key":"460_CR36","unstructured":"Rodin (2007) User Manual of the RODIN Platform. http:\/\/deploy-eprints.ecs.soton.ac.uk\/11\/1\/manual-2.3.pdf"},{"key":"460_CR37","unstructured":"Rousseau C (2006) Pr\u00e9sentation multimodale et contextuelle de l\u2019information. PhD thesis, Universit\u00e9 Paris sud XI-Orsay, France"},{"issue":"4\u20135","key":"460_CR38","doi-asserted-by":"crossref","first-page":"480","DOI":"10.1016\/j.intcom.2008.07.001","volume":"20","author":"K Song","year":"2008","unstructured":"Song K, Lee KH (2008) Generating multimodal user interfaces for Web services. Interact Comput 20(4\u20135):480\u2013490","journal-title":"Interact Comput"},{"key":"460_CR39","doi-asserted-by":"crossref","unstructured":"Westeyn T, Brashear H, Atrash A, Starner T (2003) Georgia tech gesture toolkit: Supporting experiments in gesture recognition. In: Proceedings of the 5th International Conference on Multimodal Interfaces, ACM, New York, ICMI \u201903, pp 85\u201392","DOI":"10.1145\/958432.958452"}],"container-title":["Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00607-015-0460-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00607-015-0460-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00607-015-0460-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,3]],"date-time":"2020-09-03T05:24:19Z","timestamp":1599110659000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00607-015-0460-y"}},"subtitle":["An Event-B formalization"],"short-title":[],"issued":{"date-parts":[[2015,6,10]]},"references-count":39,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2015,7]]}},"alternative-id":["460"],"URL":"https:\/\/doi.org\/10.1007\/s00607-015-0460-y","relation":{},"ISSN":["0010-485X","1436-5057"],"issn-type":[{"value":"0010-485X","type":"print"},{"value":"1436-5057","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,6,10]]}}}