{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,4]],"date-time":"2026-04-04T10:00:43Z","timestamp":1775296843857,"version":"3.50.1"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030047702","type":"print"},{"value":"9783030047719","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-030-04771-9_19","type":"book-chapter","created":{"date-parts":[[2018,12,5]],"date-time":"2018-12-05T17:02:53Z","timestamp":1544029373000},"page":"240-256","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Refinement Based Formal Development of Human-Machine Interface"],"prefix":"10.1007","author":[{"given":"Romain","family":"Geniet","sequence":"first","affiliation":[]},{"given":"Neeraj Kumar","family":"Singh","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,12,6]]},"reference":[{"key":"19_CR1","unstructured":"https:\/\/tel.archives-ouvertes.fr\/file\/index\/docid\/48279\/filename\/2_2modelesinterface_referen.html"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"Abowd, G.D., Wang, H.M., Monk, A.F.: A formal technique forautomated dialogue development. In: Proceedings of the 1st Conference on Designing Interactive Systems: Processes, Practices, Methods, & Techniques, DIS 1995, pp. 219\u2013226. ACM, New York (1995)","DOI":"10.1145\/225434.225459"},{"key":"19_CR3","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book: Assigning Programs to Meanings","author":"JR Abrial","year":"1996","unstructured":"Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)"},{"key":"19_CR4","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, New York (2010)","edition":"1"},{"issue":"6","key":"19_CR5","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in event-b. Int. J. Softw. Tools Technol. Transf. 12(6), 447\u2013466 (2010)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"Ameur, Y.A.: Cooperation of formal methods in an engineering based software development process. In: 2000 Proceedings Second International Conference Integrated Formal Methods, IFM 2000, Dagstuhl Castle, Germany, 1\u20133 November, pp. 136\u2013155 (2000)","DOI":"10.1007\/3-540-40911-4_9"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"Ameur, Y.A., A\u00eft-Sadoune, I., Mota, J., Baron, M.: 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, Montreal, Quebec, Canada, 18\u201321 April 2006, pp. 123\u2013130 (2006)","DOI":"10.1145\/1132736.1132752"},{"key":"19_CR8","unstructured":"Ameur, Y.A., Girard, P., Jambon, F.: A uniform approach for specification and design of interactive systems: the B method. In: Design, Specification and Verification of Interactive Systems 1998, Supplementary Proceedings of the Fifth International Eurographics Workshop, 3\u20135 June 1998, Abingdon, United Kingdom, pp. 51\u201367 (1998)"},{"key":"19_CR9","unstructured":"Ameur, Y.A., Girard, P., Jambon, F.: Using the B formal approach for incremental specification design of interactive systems. In: Engineering for Human-Computer Interaction, IFIP TC2\/TC13 WG2.7\/WG13.4 Seventh Working Conference on Engineering for Human-Computer Interaction, Heraklion, Crete, Greece, 14\u201318 September, pp. 91\u2013109 (1998)"},{"issue":"2","key":"19_CR10","doi-asserted-by":"publisher","first-page":"127","DOI":"10.3166\/isi.13.2.127-154","volume":"13","author":"YA Ameur","year":"2008","unstructured":"Ameur, Y.A., Sadoune, I.A., Baron, M.: Etude et comparaison de sc\u00e9narios de d\u00e9veloppements formels d\u2019interfaces multi-modales fond\u00e9s sur la preuve et le raffinement. RSTI- Ing\u00e9nierie des Syst\u00e8mes d\u2019Informations 13(2), 127\u2013155 (2008)","journal-title":"RSTI- Ing\u00e9nierie des Syst\u00e8mes d\u2019Informations"},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"Baron, M., Lucquiaud, V., Autard, D., Scapin, D.L.: K-made: Unenvironnement pour le noyau du mod\u00e8le de description del\u2019activit\u00e9. In: Proceedings of the 18th Conference onL\u2019Interaction Homme-Machine, IHM 2006, pp. 287\u2013288. ACM, New York (2006)","DOI":"10.1145\/1132736.1132786"},{"issue":"5","key":"19_CR12","doi-asserted-by":"publisher","first-page":"961","DOI":"10.1109\/TSMCA.2011.2109709","volume":"41","author":"ML Bolton","year":"2011","unstructured":"Bolton, M.L., Siminiceanu, R.I., Bass, E.J.: A systematic approach to model checking human - automation interaction using task analytic models. IEEE Trans. Syst. Man Cybern. - Part A: Syst. Hum. 41(5), 961\u2013976 (2011)","journal-title":"IEEE Trans. Syst. Man Cybern. - Part A: Syst. Hum."},{"key":"19_CR13","unstructured":"Bolton, M.L., Bass, E.J.: Building a formal model of a human-interactive system: insights into the integration of formal methods and human factors engineering. In: First NASA Formal Methods Symposium - NFM, California, USA, 6\u20138 April, pp. 6\u201315 (2009)"},{"issue":"2","key":"19_CR14","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/s11334-008-0049-0","volume":"4","author":"J Bowen","year":"2008","unstructured":"Bowen, J., Reeves, S.: Formal models for user interface design artefacts. Innov. Syst. Softw. Eng. 4(2), 125\u2013141 (2008)","journal-title":"Innov. Syst. Softw. Eng."},{"key":"19_CR15","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/j.entcs.2008.03.104","volume":"208","author":"J Bowen","year":"2008","unstructured":"Bowen, J., Reeves, S.: Refinement for user interface designs. Electron. Notes Theor. Comput. Sci. 208, 5\u201322 (2008)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-540-70569-7_6","volume-title":"Interactive Systems. Design, Specification, and Verification","author":"JC Campos","year":"2008","unstructured":"Campos, J.C., Harrison, M.D.: Systematic analysis of control panel interfaces using formal tools. In: Graham, T.C.N., Palanque, P. (eds.) DSV-IS 2008. LNCS, vol. 5136, pp. 72\u201385. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70569-7_6"},{"key":"19_CR17","doi-asserted-by":"crossref","unstructured":"Comb\u00e9fis, S., Giannakopoulou, D., Pecheur, C., Feary, M.: Learning system abstractions for human operators. In: Proceedings of the International Workshop on Machine Learning Technologies in Software Engineering, MALETS 2011, pp. 3\u201310. ACM, New York City (2011)","DOI":"10.1145\/2070821.2070822"},{"key":"19_CR18","doi-asserted-by":"crossref","unstructured":"Comb\u00e9fis, S., Pecheur, C.: A bisimulation-based approach to the analysis of human-computer interaction. In: Proceedings of the 1st ACM SIGCHI Symposium on Engineering Interactive Computing Systems, EICS 2009, pp. 101\u2013110. ACM, New York (2009)","DOI":"10.1145\/1570433.1570454"},{"key":"19_CR19","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-1-5041-2896-4_19","volume-title":"Human-Computer Interaction","author":"J Coutaz","year":"1995","unstructured":"Coutaz, J., Nigay, L., Salber, D., Blandford, A., May, J., Young, R.M.: Four easy pieces for assessing the usability of multimodal interaction: the care properties. In: Nordby, K., Helmersen, P., Gilmore, D.J., Arnesen, S.A. (eds.) Human-Computer Interaction. IFIP Advances in Information and Communication Technology, pp. 115\u2013120. Springer, Boston (1995). https:\/\/doi.org\/10.1007\/978-1-5041-2896-4_19"},{"key":"19_CR20","volume-title":"Human-Computer Interaction","author":"A Dix","year":"2003","unstructured":"Dix, A., Finlay, J.E., Abowd, G.D., Beale, R.: Human-Computer Interaction, 3rd edn. Prentice-Hall Inc., Upper Saddle River (2003)","edition":"3"},{"key":"19_CR21","unstructured":"EB2ALL: An automatic code generation tool from Event-B (2011). http:\/\/eb2all.loria.fr\/"},{"key":"19_CR22","volume-title":"Formal Description Technique Lotos: Results of the Esprit Sedos Project","year":"1989","unstructured":"Eijk, P.V., Diaz, M. (eds.): Formal Description Technique Lotos: Results of the Esprit Sedos Project. Elsevier Science Inc., New York (1989)"},{"issue":"2","key":"19_CR23","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1518\/001872007X312522","volume":"49","author":"M Heymann","year":"2007","unstructured":"Heymann, M., Degani, A.: Formal analysis and automatic generation of user interfaces: approach, methodology, and an algorithm. Hum. Factors 49(2), 311\u2013330 (2007)","journal-title":"Hum. Factors"},{"key":"19_CR24","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-94-010-0421-3_4","volume-title":"Computer-Aided Design of User Interfaces III","author":"Francis Jambon","year":"2002","unstructured":"Jambon, F.: From formal specifications to secure implementations. In: Proceedings of the Fourth International Conference on Computer-Aided Design of User Interfaces III, Valenciennes, France, 15\u201317 May 2002, pp. 51\u201362 (2002)"},{"key":"19_CR25","unstructured":"Lecrubier, V.: A formal language for designing, specifying and verifying critical embedded human machine interfaces. Theses, INSTITUT SUPERIEUR DE L\u2019AERONAUTIQUE ET DE L\u2019ESPACE (ISAE); UNIVERSITE DE TOULOUSE, June 2016. https:\/\/hal.archives-ouvertes.fr\/tel-01455466"},{"key":"19_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003: Formal Methods","author":"M Leuschel","year":"2003","unstructured":"Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855\u2013874. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45236-2_46"},{"issue":"6","key":"19_CR27","doi-asserted-by":"publisher","first-page":"822","DOI":"10.1109\/THMS.2017.2700630","volume":"47","author":"M Li","year":"2017","unstructured":"Li, M., Wei, J., Zheng, X., Bolton, M.L.: A formal machine-learning approach to generating human-machine interfaces from task models. IEEE Trans. Hum.-Mach. Syst. 47(6), 822\u2013833 (2017)","journal-title":"IEEE Trans. Hum.-Mach. Syst."},{"key":"19_CR28","doi-asserted-by":"crossref","unstructured":"M\u00e9ry, D., Singh, N.K.: Automatic code generation from event-b models. In: Proceedings of the Second Symposium on Information and Communication Technology, SoICT 2011, pp. 179\u2013188. ACM, New York (2011)","DOI":"10.1145\/2069216.2069252"},{"key":"19_CR29","unstructured":"Mohand Oussa\u00efd, L.M.O.: Formal modelling and verification of multimodal human computer interfaces : output multimodality. Theses, ISAE-ENSMA Ecole Nationale Sup\u00e9rieure de M\u00e9canique et d\u2019A\u00e9rotechique - Poitiers, December 2014. https:\/\/tel.archives-ouvertes.fr\/tel-01127547"},{"key":"19_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/3-540-45522-1_6","volume-title":"Interactive Systems: Design, Specification, and Verification","author":"D Navarre","year":"2001","unstructured":"Navarre, D., Palanque, P., Patern\u00f2, F., Santoro, C., Bastide, R.: A tool suite for integrating task and system models through scenarios. In: Johnson, C. (ed.) DSV-IS 2001. LNCS, vol. 2220, pp. 88\u2013113. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45522-1_6"},{"key":"19_CR31","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-0-387-34907-7_11","volume-title":"Engineering for Human-Computer Interaction","author":"P Palanque","year":"1996","unstructured":"Palanque, P., Bastide, R., Seng\u00e8s, V.: Validating interactive system design through the verification of formal task and system models. In: Bass, L.J., Unger, C. (eds.) EHCI 1995. IFIP Advances in Information and Communication Technology, pp. 189\u2013212. Springer, Boston (1996). https:\/\/doi.org\/10.1007\/978-0-387-34907-7_11"},{"key":"19_CR32","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-642-87115-3_23","volume-title":"Interactive Systems: Design, Specification, and Verification Focus on Computer Graphics (Tutorials and Perspectives in Computer Graphics)","author":"PA Palanque","year":"1995","unstructured":"Palanque, P.A., Bastide, R.: Petri net based design of user-driven interfaces using the interactive cooperative objects formalism. In: Patern\u00f3, F. (ed.) Interactive Systems: Design, Specification, and Verification Focus on Computer Graphics (Tutorials and Perspectives in Computer Graphics), pp. 383\u2013400. Springer, Berlin (1995). https:\/\/doi.org\/10.1007\/978-3-642-87115-3_23"},{"key":"19_CR33","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-1-5041-2896-4_32","volume-title":"Human\u2014Computer Interaction","author":"P Palanque","year":"1995","unstructured":"Palanque, P., Bastide, R.: Verification of an interactive software by analysis of its formal specification. In: Nordby, K., Helmersen, P., Gilmore, D.J., Arnesen, S.A. (eds.) Human\u2014Computer Interaction. IFIP Advances in Information and Communication Technology, pp. 191\u2013196. Springer, Boston (1995). https:\/\/doi.org\/10.1007\/978-1-5041-2896-4_32"},{"key":"19_CR34","unstructured":"Reenskaug, T.M.H.: The original MVC reports (1979)"},{"key":"19_CR35","unstructured":"Ruksenas, R., Masci, P., Harrison, M.D., Curzon, P.: Developing and verifying user interface requirements for infusion pumps: a refinement approach. ECEASST, 69 (2013). ISSN: 1863-2122"},{"key":"19_CR36","doi-asserted-by":"crossref","unstructured":"Pinheiro da Silva, P., Griffiths, T., Paton, N.W.: Generating user interface code in a model based user interface development environment. In: Proceedings of the Working Conference on Advanced Visual Interfaces, AVI 2000, pp. 155\u2013160. ACM, New York (2000)","DOI":"10.1145\/345513.345301"},{"key":"19_CR37","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-5260-6","volume-title":"Using Event-B for Critical Device Software Systems","author":"NK Singh","year":"2013","unstructured":"Singh, N.K.: Using Event-B for Critical Device Software Systems. Springer, Heidelberg (2013)"}],"container-title":["Lecture Notes in Computer Science","Software Technologies: Applications and Foundations"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-04771-9_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,4]],"date-time":"2026-04-04T09:26:04Z","timestamp":1775294764000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-04771-9_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030047702","9783030047719"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-04771-9_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"STAF","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Federation of International Conferences on Software Technologies: Applications and Foundations","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Toulouse","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 June 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 June 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"staf2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.staf2018.fr\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}