{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,2]],"date-time":"2025-07-02T22:23:55Z","timestamp":1751495035022,"version":"3.40.3"},"publisher-location":"Cham","reference-count":205,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319518374"},{"type":"electronic","value":"9783319518381"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-51838-1_1","type":"book-chapter","created":{"date-parts":[[2017,4,24]],"date-time":"2017-04-24T08:23:43Z","timestamp":1493022223000},"page":"3-55","source":"Crossref","is-referenced-by-count":8,"title":["State of the Art on Formal Methods for Interactive Systems"],"prefix":"10.1007","author":[{"given":"Raquel","family":"Oliveira","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Philippe","family":"Palanque","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Benjamin","family":"Weyers","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Judy","family":"Bowen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan","family":"Dix","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,4,25]]},"reference":[{"key":"1_CR1","unstructured":"Abowd GD (1991) Formal aspects of human-computer interaction. Dissertation, University of Oxford"},{"issue":"3","key":"1_CR2","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1016\/0953-5438(92)90021-7","volume":"4","author":"GD Abowd","year":"1992","unstructured":"Abowd GD, Dix AJ (1992) Giving undo attention. Interact Comput 4(3):317\u2013342","journal-title":"Interact Comput"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Abowd GD, Wang H-M, Monk AF (1995) A formal technique for automated dialogue development. In: Proceedings of the 1st conference on designing interactive systems: processes, practices, methods, & techniques. ACM, pp 219\u2013226","DOI":"10.1145\/225434.225459"},{"key":"1_CR4","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-book: Assigning Programs to Meanings","author":"J-R Abrial","year":"1996","unstructured":"Abrial J-R (1996) The B-book: Assigning Programs to Meanings. Cambridge University Press, New York"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Acharya C, Thimbleby HW, Oladimeji P (2010) Human computer interaction and medical devices. In: Proceedings of the 2010 british computer society conference on human-computer interaction, pp 168\u2013176","DOI":"10.14236\/ewic\/HCI2010.22"},{"key":"1_CR6","unstructured":"A\u00eft-Ameur Y, Girard P, Jambon F (1998a) A uniform approach for specification and design of interactive systems: the B method. In: Proceedings of the fifth international eurographics workshop on design, specification and verification of interactive systems, pp 51\u201367"},{"key":"1_CR7","unstructured":"A\u00eft-Ameur Y, Girard P, Jambon F (1998b) A uniform approach for the specification and design of interactive systems: the B method. In: Eurographics workshop on design, specification, and verification of interactive systems, pp 333\u2013352"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"A\u00eft-Ameur Y, Girard P, Jambon F (1999) Using the B formal approach for incremental specification design of interactive systems. In: Engineering for human-computer interaction. Springer, pp 91\u2013109","DOI":"10.1007\/978-0-387-35349-4_6"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"A\u00eft-Ameur Y (2000) Cooperation of formal methods in an engineering based software development process. In: Proceedings of integrated formal methods, second international conference, pp 136\u2013155","DOI":"10.1007\/3-540-40911-4_9"},{"key":"1_CR10","unstructured":"A\u00eft-Ameur Y, Baron M, Girard P (2003a) Formal validation of HCI user tasks. In: Software engineering research and practice, pp 732\u2013738"},{"key":"1_CR11","unstructured":"A\u00eft-Ameur Y, Baron M, Kamel N (2003b) Utilisation de Techniques Formelles dans la Modelisation d\u2019Interfaces Homme-machine. Une Experience Comparative entre B et Promela\/SPIN. In: 6th International Symposium on Programming and Systems, p 57\u201366"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"A\u00eft-Ameur Y, Kamel N (2004) A generic formal specification of fusion of modalities in a multimodal HCI. In: Building the information society. Springer, pp 415\u2013420","DOI":"10.1007\/978-1-4020-8157-6_34"},{"key":"1_CR13","unstructured":"A\u00eft-Ameur Y, Baron M (2004) Bridging the gap between formal and experimental validation approaches in HCI systems design: use of the event B proof based technique. In: International symposium on leveraging applications of formal methods, pp 74\u201380"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"A\u00eft-Ameur Y, Breholee B, Girard P, Guittet L, Jambon F (2004) Formal verification and validation of interactive systems specifications. In: Human error, safety and systems development. Springer, p 61\u201376","DOI":"10.1007\/1-4020-8153-7_5"},{"key":"1_CR15","unstructured":"A\u00eft-Ameur Y, Baron M, Kamel N (2005a) Encoding a Process Algebra Using the Event B Method. Application to the Validation of User Interfaces. In: Proceedings of 2nd IEEE international symposium on leveraging applications of formal methods, p 1\u201317"},{"key":"1_CR16","unstructured":"A\u00eft-Ameur Y, Idir A-S, Mickael B (2005b) Modelisation et Validation formelles d\u2019IHM: LOT 1 (LISI\/ENSMA). Technical report. LISI\/ENSMA"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"A\u00eft-Ameur Y, A\u00eft-Sadoune I, Mota J-M, Baron M (2006) Validation et Verification Formelles de Systemes Interactifs Multi-modaux Fondees sur la Preuve. In: Proceedings of the 18th International Conference of the Association Francophone d\u2019Interaction Homme-Machine, pp 123\u2013130","DOI":"10.1145\/1132736.1132752"},{"issue":"6","key":"1_CR18","doi-asserted-by":"crossref","first-page":"547","DOI":"10.1007\/s10009-006-0008-8","volume":"8","author":"Y A\u00eft-Ameur","year":"2006","unstructured":"A\u00eft-Ameur Y, Baron M (2006) Formal and experimental validation approaches in HCI systems design based on a shared event B model. Int J Softw Tools Technol Transf 8(6):547\u2013563","journal-title":"Int J Softw Tools Technol Transf"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"A\u00eft-Sadoune I, A\u00eft-Ameur Y (2008) Animating event B models by formal data models. In: Proceedings of leveraging applications of formal methods, verification and validation, pp 37\u201355","DOI":"10.1007\/978-3-540-88479-8_4"},{"issue":"3","key":"1_CR20","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1007\/s10009-009-0109-2","volume":"11","author":"Y A\u00eft-Ameur","year":"2009","unstructured":"A\u00eft-Ameur Y, Baron M, Kamel N, Mota J-M (2009) Encoding a process algebra using the event B method. Int J Softw Tools Technol Transfer 11(3):239\u2013253","journal-title":"Int J Softw Tools Technol Transfer"},{"issue":"1","key":"1_CR21","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s10009-009-0131-4","volume":"12","author":"Y A\u00eft-Ameur","year":"2010","unstructured":"A\u00eft-Ameur Y, Boniol F, Wiels V (2010a) Toward a wider use of formal methods for aerospace systems design and verification. Int J Softw Tools Technol Transf 12(1):1\u20137","journal-title":"Int J Softw Tools Technol Transf"},{"issue":"1","key":"1_CR22","doi-asserted-by":"crossref","first-page":"1","DOI":"10.5753\/jis.2010.559","volume":"1","author":"Y A\u00eft-Ameur","year":"2010","unstructured":"A\u00eft-Ameur Y, A\u00eft-Sadoune I, Baron M, Mota J-M (2010b) Verification et Validation Formelles de Systemes Interactifs Fondees sur la Preuve: Application aux Systemes Multi-Modaux. J Interact Pers Syst 1(1):1\u201330","journal-title":"J Interact Pers Syst"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"A\u00eft-Ameur Y, Gibson JP, Mery D (2014) On implicit and explicit semantics: integration issues in proof-based development of systems. In: Leveraging applications of formal methods, verification and validation. Specialized techniques and applications. Springer, p 604\u2013618","DOI":"10.1007\/978-3-662-45231-8_50"},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"Barboni E, Ladry J-F, Navarre D, Palanque PA, Winckler M (2010) Beyond modelling: an integrated environment supporting co-execution of tasks and systems models. In: Proceedings of ACM EICS conference, pp 165\u2013174","DOI":"10.1145\/1822018.1822043"},{"issue":"5","key":"1_CR25","doi-asserted-by":"crossref","first-page":"545","DOI":"10.1016\/j.ssci.2007.01.001","volume":"45","author":"S Basnyat","year":"2007","unstructured":"Basnyat S, Palanque PA, Schupp B, Wright P (2007) Formal socio-technical barrier modelling for safety-critical interactive systems design. Saf Sci 45(5):545\u2013565","journal-title":"Saf Sci"},{"key":"1_CR26","unstructured":"Bass L, Little R, Pellegrino R, Reed S, Seacord R, Sheppard S, Szezur MR (1991) The ARCH model: seeheim revisited. In: User interface developpers\u2019 workshop"},{"key":"1_CR27","unstructured":"Bastide R, Palanque PA (1990) Petri net objects for the design, validation and prototyping of user-driven interfaces. In: IFIP INTERACT 1990 conference, pp 625\u2013631"},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Bastide R, Navarre D, Palanque PA (2002) A model-based tool for interactive prototyping of highly interactive applications. In: CHI extended abstracts, pp 516\u2013517","DOI":"10.1145\/506443.506457"},{"issue":"3","key":"1_CR29","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1016\/S0953-5438(03)00011-0","volume":"15","author":"R Bastide","year":"2003","unstructured":"Bastide R, Navarre D, Palanque PA (2003) A tool-supported design framework for safety critical interactive systems. Interact Comput 15(3):309\u2013328","journal-title":"Interact Comput"},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"Bastide R, Navarre D, Palanque PA, Schyn A, Dragicevic P (2004) A model-based approach for real-time embedded multimodal systems in military aircrafts. In: Proceedings of the 6th international conference on multimodal interfaces, pp 243\u2013250","DOI":"10.1145\/1027933.1027974"},{"key":"1_CR31","doi-asserted-by":"crossref","unstructured":"Beck K (1999) Extreme programming explained: embrace change. Addison-Wesley","DOI":"10.1109\/TOOLS.1999.779100"},{"key":"1_CR32","volume-title":"The unified modelling language user guide","author":"G Booch","year":"2005","unstructured":"Booch G (2005) The unified modelling language user guide. Pearson Education, India"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"Bourguet-Rouger A (1988) External behaviour equivalence between two petri nets. In: Proceedings of concurrency. Lecture notes in computer science, vol 335. Springer, pp 237\u2013256","DOI":"10.1007\/3-540-50403-6_43"},{"key":"1_CR34","doi-asserted-by":"crossref","unstructured":"Bowen J, Reeves S (2006) Formal refinement of informal GUI design artefacts. In: Proceedings of 17th Australian software engineering conference, pp 221\u2013230","DOI":"10.1109\/ASWEC.2006.28"},{"key":"1_CR35","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1016\/j.entcs.2007.01.061","volume":"183","author":"J Bowen","year":"2007","unstructured":"Bowen J, Reeves S (2007a) Formal models for informal GUI designs. Electr Notes Theor Comput Sci 183:57\u201372","journal-title":"Electr Notes Theor Comput Sci"},{"key":"1_CR36","doi-asserted-by":"crossref","unstructured":"Bowen J, Reeves S (2007b) using formal models to design user interfaces: a case study. In: Proceedings of the 21st British HCI group annual conference on HCI, pp 159\u2013166","DOI":"10.14236\/ewic\/HCI2007.16"},{"key":"1_CR37","doi-asserted-by":"crossref","unstructured":"Bowen J, Reeves S (2012) Modelling user manuals of modal medical devices and learning from the experience. In: Proceedings of ACM SIGCHI symposium on engineering interactive computing systems, pp 121\u2013130","DOI":"10.1145\/2305484.2305505"},{"issue":"3","key":"1_CR38","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1007\/s11334-013-0199-6","volume":"9","author":"J Bowen","year":"2013","unstructured":"Bowen J, Reeves S (2013) UI-design driven model-based testing. Innov Syst Softw Eng 9(3):201\u2013215","journal-title":"Innov Syst Softw Eng"},{"key":"1_CR39","doi-asserted-by":"crossref","unstructured":"Bowen J (2015) Creating models of interactive systems with the support of lightweight reverse-engineering tools. In: Proceedings of the 7th ACM SIGCHI symposium on engineering interactive computing systems, pp 110\u2013119","DOI":"10.1145\/2774225.2774840"},{"key":"1_CR40","doi-asserted-by":"crossref","unstructured":"Boyer RS, Moore JS (1983) Proof-checking, theorem proving, and program verification. Technical report, DTIC document","DOI":"10.1090\/conm\/029\/07"},{"key":"1_CR41","doi-asserted-by":"crossref","unstructured":"Brat G, Martinie C, Palanque P (2013) V&V of lexical, syntactic and semantic properties for interactive systems through model checking of formal description of dialog. In: Proceedings of the 15th international conference on human-computer interaction, pp 290\u2013299","DOI":"10.1007\/978-3-642-39232-0_33"},{"key":"1_CR42","doi-asserted-by":"crossref","unstructured":"Bumbulis P, Alencar PSC, Cowan DD, Lucena CJP (1995a) Combining formal techniques and prototyping in user interface construction and verification. In: Proceedings of 2nd eurographics workshop on design, specification, verification of interactive systems, pp 7\u20139","DOI":"10.1007\/978-3-7091-9437-9_11"},{"key":"1_CR43","doi-asserted-by":"crossref","unstructured":"Bumbulis P, Alencar PSC, Cowan DD, de Lucena CJP (1995b) A framework for machine-assisted user interface verification. In: Proceedings of the 4th international conference on algebraic methodology and software technology, pp 461\u2013474","DOI":"10.1007\/3-540-60043-4_71"},{"issue":"2","key":"1_CR44","doi-asserted-by":"crossref","first-page":"346","DOI":"10.1016\/j.apergo.2013.04.017","volume":"45","author":"D Burkolter","year":"2014","unstructured":"Burkolter D, Weyers B, Kluge A, Luther W (2014) Customization of user interfaces to reduce errors and enhance user acceptance. Appl Ergon 45(2):346\u2013353","journal-title":"Appl Ergon"},{"key":"1_CR45","doi-asserted-by":"crossref","unstructured":"Campos JC, Harrison MD (1997) Formally verifying interactive systems: a review. In: Proceedings of design, specification and verification of interactive systems, pp 109\u2013124","DOI":"10.1007\/978-3-7091-6878-3_8"},{"key":"1_CR46","unstructured":"Campos JC (1999) Automated deduction and usability reasoning. Dissertatoin, University of York"},{"issue":"3\u20134","key":"1_CR47","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1023\/A:1011265604021","volume":"8","author":"JC Campos","year":"2001","unstructured":"Campos JC, Harrison MD (2001) Model checking interactor specifications. Autom Softw Eng 8(3\u20134):275\u2013310","journal-title":"Autom Softw Eng"},{"key":"1_CR48","unstructured":"Campos JC, Harrison MD (2007) Considering context and users in interactive systems analysis. In: Proceedings of the joint working conferences on engineering interactive systems, pp 193\u2013209"},{"key":"1_CR49","doi-asserted-by":"crossref","unstructured":"Campos JC, Harrison MD (2008) Systematic analysis of control panel interfaces using formal tools. In: Interactive systems. Design, specification, and verification. Springer, pp 72\u201385","DOI":"10.1007\/978-3-540-70569-7_6"},{"key":"1_CR50","doi-asserted-by":"crossref","unstructured":"Campos JC, Harrison MD (2009) Interaction engineering using the IVY tool. In: Proceedings of the 1st ACM SIGCHI symposium on engineering interactive computing systems, pp 35\u201344","DOI":"10.1145\/1570433.1570442"},{"key":"1_CR51","unstructured":"Campos JC, Harrison MD (2011) Modelling and analysing the interactive behaviour of an infusion pump. Electron Commun EASST 45"},{"key":"1_CR53","doi-asserted-by":"crossref","unstructured":"Cauchi A, Gimblett A, Thimbleby HW, Curzon P, Masci P (2012a) Safer \u201c5-key\u201d number entry user interfaces using differential formal analysis. In: Proceedings of the 26th annual BCS interaction specialist group conference on people and computers, pp 29\u201338","DOI":"10.14236\/ewic\/HCI2012.8"},{"key":"1_CR54","doi-asserted-by":"crossref","unstructured":"Cauchi A, Gimblett A, Thimbleby HW, Curzon P, Masci P (2012b) Safer \u201c5-key\u201d number entry user interfaces using differential formal analysis. In: Proceedings of the 26th annual BCS interaction specialist group conference on people and computers, pp 29\u201338","DOI":"10.14236\/ewic\/HCI2012.8"},{"key":"1_CR55","doi-asserted-by":"crossref","unstructured":"Cauchi A, Oladimeji P, Niezen G, Thimbleby HW (2014) triangulating empirical and analytic techniques for improving number entry user interfaces. In: Proceedings of ACM SIGCHI symposium on engineering interactive computing systems, pp 243\u2013252","DOI":"10.1145\/2607023.2607025"},{"key":"1_CR56","unstructured":"Champelovier D, Clerc X, Garavel H, Guerte Y, Lang F, Serwe W, Smeding G (2010) Reference manual of the LOTOS NT to LOTOS translator (version 5.0). INRIA\/VASY"},{"issue":"1","key":"1_CR57","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1145\/320434.320440","volume":"1","author":"P Chen","year":"1976","unstructured":"Chen P (1976) The entity-relationship model\u2014toward a unified view of data. ACM Trans Database Syst 1(1):9\u201336","journal-title":"ACM Trans Database Syst"},{"issue":"2","key":"1_CR58","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke EM, Emerson EA, Sistla AP (1986) Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans Program Lang Syst 8(2):244\u2013263","journal-title":"ACM Trans Program Lang Syst"},{"key":"1_CR59","doi-asserted-by":"crossref","unstructured":"Cofer D, Whalen M, Miller S (2008) Software model checking for avionics systems. In: Digital avionics systems conference, pp 1\u20138","DOI":"10.1109\/DASC.2008.4702862"},{"key":"1_CR60","doi-asserted-by":"crossref","unstructured":"Cofer D (2010) Model checking: cleared for take-off. In: Model checking software. Springer, pp 76\u201387","DOI":"10.1007\/978-3-642-16164-3_6"},{"key":"1_CR61","doi-asserted-by":"crossref","unstructured":"Cofer D (2012) Formal methods in the aerospace industry: follow the money. In: Proceedings of the 14th international conference on formal engineering methods: formal methods and software engineering. Springer, pp 2\u20133","DOI":"10.1007\/978-3-642-34281-3_2"},{"key":"1_CR62","doi-asserted-by":"crossref","unstructured":"Cofer D, Gacek A, Miller S, Whalen MW, LaValley B, Sha L (2012) Compositional verification of architectural models. In: Proceedings of the 4th international conference on NASA formal methods. Springer, pp 126\u2013140","DOI":"10.1007\/978-3-642-28891-3_13"},{"key":"1_CR63","doi-asserted-by":"crossref","unstructured":"Combefis S, Pecheur C (2009) A bisimulation-based approach to the analysis of human-computer interaction. In: Proceedings of the 1st ACM SIGCHI symposium on engineering interactive computing systems, pp 101\u2013110","DOI":"10.1145\/1570433.1570454"},{"key":"1_CR64","doi-asserted-by":"crossref","unstructured":"Comb\u00e9fis S, Giannakopoulou D, Pecheur C, Feary M (2011a) A formal framework for design and analysis of human-machine interaction. In: Proceedings of the IEEE international conference on systems, man and cybernetics, pp 1801\u20131808","DOI":"10.1109\/ICSMC.2011.6083933"},{"key":"1_CR65","doi-asserted-by":"crossref","unstructured":"Comb\u00e9fis S, Giannakopoulou D, Pecheur C, Feary M (2011b) Learning system abstractions for human operators. In: Proceedings of the international workshop on machine learning technologies in software engineering, pp 3\u201310","DOI":"10.1145\/2070821.2070822"},{"key":"1_CR66","unstructured":"Comb\u00e9fis S (2013) A formal framework for the analysis of human-machine interactions. Dissertation, Universite catholique de Louvain"},{"key":"1_CR67","doi-asserted-by":"crossref","unstructured":"Cortier A, d\u2019Ausbourg B, A\u00eft-Ameur Y (2007) Formal validation of java\/swing user interfaces with the event B method. In: Human-computer interaction. Interaction design and usability. Springer, pp 1062\u20131071","DOI":"10.1007\/978-3-540-73105-4_116"},{"key":"1_CR68","doi-asserted-by":"crossref","unstructured":"Coutaz J (1987) PAC, an object oriented model for dialogue design. In: Bullinger H-J, Shackel B (eds) Human computer interaction INTERACT\u201987, pp 431\u2013436","DOI":"10.1016\/B978-0-444-70304-0.50074-1"},{"key":"1_CR69","first-page":"461","volume":"2004","author":"P Curzon","year":"2004","unstructured":"Curzon P, Blandford A (2004) Formally justifying user-centred design rules: a case study on post-completion errors. Proc IFM 2004:461\u2013480","journal-title":"Proc IFM"},{"key":"1_CR70","doi-asserted-by":"crossref","unstructured":"d\u2019Ausbourg B (1998) Using model checking for the automatic validation of user interface systems. In: Proceedings of the fifth international eurographics workshop on the design, specification and verification of interactive systems, pp 242\u2013260","DOI":"10.1007\/978-3-7091-3693-5_16"},{"key":"1_CR71","doi-asserted-by":"crossref","unstructured":"d\u2019Ausbourg B, Seguin C, Durrieu G, Roche P (1998) Helping the automated validation process of user interfaces systems. In: Proceedings of the 20th international conference on software engineering, p 219\u2013228","DOI":"10.1109\/ICSE.1998.671121"},{"key":"1_CR72","unstructured":"d\u2019Ausbourg B (2002) Synthetiser I\u2019Intention d\u2019un Pilote pour Definir de Nouveaux \u00c9quipements de Bord. In: Proceedings of the 14th French-speaking Conference on Human-computer Interaction, pp 145\u2013152"},{"key":"1_CR73","doi-asserted-by":"crossref","unstructured":"De Moura L, Owre S, Rue\u00df H, Rushby J, Shankar N, Sorea M, Tiwari A (2004) SAL 2. In: Proceeidngs of computer aided verification, pp 496\u2013500","DOI":"10.1007\/978-3-540-27813-9_45"},{"issue":"1","key":"1_CR74","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1518\/0018720024494838","volume":"44","author":"A Degani","year":"2002","unstructured":"Degani A, Heymann M (2002) Formal verification of human-automation interaction. Hum Fact J Hum Fact Ergon Soc 44(1):28\u201343","journal-title":"Hum Fact J Hum Fact Ergon Soc"},{"key":"1_CR75","unstructured":"Dey T (2011) A comparative analysis on modelling and implementing with MVC architecture. In: Proceedings of the international conference on web services computing, vol 1, pp 44\u201349"},{"key":"1_CR76","unstructured":"Dix AJ (1988) Abstract, generic models of interactive systems. In: Proceedings of fourth conference of the british computer society human-computer interaction specialist group. University of Manchester, pp 63\u201377"},{"key":"1_CR77","doi-asserted-by":"crossref","unstructured":"Dix AJ, Harrison MD, Cunciman R, Thimbleby HW (1987) interaction models and the principled design of interactive systems. In: Proceedings of the 1st European software engineering conference, pp 118\u2013126","DOI":"10.1007\/BFb0022105"},{"key":"1_CR78","volume-title":"Formal methods for Interactive systems","author":"AJ Dix","year":"1991","unstructured":"Dix AJ (1991) Formal methods for Interactive systems. Academic Press, London"},{"key":"1_CR79","first-page":"9","volume-title":"Perspectives on HCI: diverse approaches","author":"AJ Dix","year":"1995","unstructured":"Dix AJ (1995) Formal Methods. In: Monk A, Gilbert N (eds) Perspectives on HCI: diverse approaches. Academic Press, London, pp 9\u201343"},{"key":"1_CR80","unstructured":"Dix AJ (2012) Formal methods. In: Soegaard M, Dam R (eds) Encyclopedia of human-computer interaction"},{"key":"1_CR81","doi-asserted-by":"crossref","first-page":"260","DOI":"10.1007\/PL00003934","volume":"12","author":"G Doherty","year":"1998","unstructured":"Doherty G, Campos JC, Harrison MD (1998) Representational reasoning and verification. Formal Aspects Comput 12:260\u2013277","journal-title":"Formal Aspects Comput"},{"key":"1_CR82","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1111\/1467-8659.1230025","volume":"12","author":"DJ Duke","year":"1993","unstructured":"Duke DJ, Harrison MD (1993) Abstract interaction objects. Comput Graph Forum 12:25\u201336","journal-title":"Comput Graph Forum"},{"issue":"1","key":"1_CR83","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1049\/sej.1995.0002","volume":"10","author":"DJ Duke","year":"1995","unstructured":"Duke DJ, Harrison MD (1995) Event model of human-system interaction. Softw Eng J 10(1):3\u201312","journal-title":"Softw Eng J"},{"key":"1_CR84","unstructured":"Elder MC, Knight J (1995) specifying user interfaces for safety-critical medical systems. In: Proceedings of the 2nd annual international symposium on medical robotics and computer assisted surgery, pp 148\u2013155"},{"key":"1_CR85","doi-asserted-by":"crossref","unstructured":"Fahssi R, Martinie C, Palanque PA (2015) Enhanced task modelling for systematic identification and explicit representation of human errors. In: Proceedings of INTERACT, pp 192\u2013212","DOI":"10.1007\/978-3-319-22723-8_16"},{"key":"1_CR86","doi-asserted-by":"crossref","unstructured":"Fields B, Wright P, Harrison M (1995) Applying formal methods for human error tolerant design. In: Software engineering and human-computer interaction. Springer, pp 185\u2013195","DOI":"10.1007\/BFb0035815"},{"issue":"3","key":"1_CR87","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1145\/988026.988037","volume":"8","author":"JD Foley","year":"1974","unstructured":"Foley JD, Wallace VL (1974) The art of natural graphic man-machine conversation. Comput Graph\u00a08(3):87","journal-title":"Comput Graph"},{"key":"1_CR88","unstructured":"Garavel H, Graf S (2013) formal methods for safe and secure computer systems. Federal office for information security"},{"issue":"2","key":"1_CR89","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/s10009-012-0244-z","volume":"15","author":"H Garavel","year":"2013","unstructured":"Garavel H, Lang F, Mateescu R, Serwe W (2013) CADP 2011: a toolbox for the construction and analysis of distributed processes. Int J Softw Tools Technol Transf 15(2):89\u2013107","journal-title":"Int J Softw Tools Technol Transf"},{"key":"1_CR90","doi-asserted-by":"crossref","unstructured":"Gimblett A, Thimbleby HW (2010) User interface model discovery: towards a generic approach. In: Proceedings of the 2nd ACM SIGCHI symposium on engineering interactive computing system, EICS 2010, Berlin, Germany, pp 145\u2013154","DOI":"10.1145\/1822018.1822041"},{"key":"1_CR91","doi-asserted-by":"crossref","unstructured":"Gimblett A, Thimbleby HW (2013) Applying theorem discovery to automatically find and check usability heuristics. In: Proceedings of the 5th ACM SIGCHI symposium on engineering interactive computing systems, pp 101\u2013106","DOI":"10.1145\/2494603.2480320"},{"issue":"4","key":"1_CR92","first-page":"15","volume":"1","author":"P Hallinger","year":"2000","unstructured":"Hallinger P, Crandall DP, Seong DNF (2000) Systems thinking\/systems changing & a computer simulation for learning how to make school smarter. Adv Res Theor School Manag Educ Policy 1(4):15\u201324","journal-title":"Adv Res Theor School Manag Educ Policy"},{"key":"1_CR93","doi-asserted-by":"crossref","unstructured":"Hamilton D, Covington R, Kelly J, Kirkwood C, Thomas M, Flora-Holmquist AR, Staskauskas MG, Miller SP, Srivas MK, Cleland G, MacKenzie D (1995) Experiences in applying formal methods to the analysis of software and system requirements. In: Workshop on industrial-strength formal specification techniques, pp 30\u201343","DOI":"10.1109\/WIFT.1995.515477"},{"key":"1_CR94","doi-asserted-by":"crossref","unstructured":"Hamon A, Palanque PA, Silva JL, Deleris Y, Barboni E (2013) Formal description of multi-touch interactions. In: Proceedings of the 5th ACM SIGCHI symposium on engineering interactive computing systems, pp 207\u2013216","DOI":"10.1145\/2494603.2480311"},{"key":"1_CR95","doi-asserted-by":"crossref","unstructured":"Hardin DS, Hiratzka TD, Johnson DR, Wagner L, Whalen MW (2009) Development of security software: a high assurance methodology. In: Proceedings of 11th international conference on formal engineering methods, pp 266\u2013285","DOI":"10.1007\/978-3-642-10373-5_14"},{"key":"1_CR96","unstructured":"Harrison M, Thimbleby HW (eds) (1990) Formal methods in HCI. Cambridge University Press"},{"key":"1_CR97","doi-asserted-by":"crossref","unstructured":"Harrison MD, Duke DJ (1995) A review of formalisms for describing interactive behaviour. In: software engineering and human-computer interaction. Springer, pp 49\u201375","DOI":"10.1007\/BFb0035807"},{"key":"1_CR98","unstructured":"Harrison MD, Masci P, Campos JC, Curzon P (2013) Automated theorem proving for the systematic analysis of an infusion pump. Electron Commun EASST69"},{"key":"1_CR99","doi-asserted-by":"crossref","unstructured":"Harrison MD, Campos JC, Masci P (2015) Reusing models and properties in the analysis of similar interactive devices, pp 95\u2013111","DOI":"10.1007\/s11334-013-0201-3"},{"key":"1_CR100","volume-title":"Developing user interfaces: ensuring usability through product process","author":"D Hix","year":"1993","unstructured":"Hix D, Hartson RH (1993) Developing user interfaces: ensuring usability through product process. Wiley, New York"},{"key":"1_CR101","unstructured":"ISO\/IEC (1989) LOTOS\u2014a formal description technique based on the temporal ordering of observational behaviour. International Standard 8807"},{"key":"1_CR102","first-page":"2001","volume":"15437","author":"ISO IEC","year":"2001","unstructured":"IEC ISO (2001) Enhancements to LOTOS (E-LOTOS). Int Stand 15437:2001","journal-title":"Int Stand"},{"key":"1_CR103","unstructured":"ISO\/IEC (2002) 13568, Information technology\u2014Z formal specification notation\u2014syntax, type system and semantics"},{"key":"1_CR104","doi-asserted-by":"crossref","unstructured":"Jambon F, Girard P, A\u00eft-Ameur Y (2001) Interactive system safety and usability enforced with the development process. In: Proceedings of 8th IFIP international conference on engineering for human-computer interaction, pp 39\u201356","DOI":"10.1007\/3-540-45348-2_8"},{"key":"1_CR105","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1016\/S0020-7373(85)80045-6","volume":"22","author":"DE Kieras","year":"1985","unstructured":"Kieras DE, Polson PG (1985) An approach to the formal analysis of user complexity. Int J Man Mach Stud 22:94\u2013365","journal-title":"Int J Man Mach Stud"},{"issue":"2","key":"1_CR106","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1504\/IJHFE.2014.067819","volume":"3","author":"A Kluge","year":"2014","unstructured":"Kluge A, Greve J, Borisov N, Weyers B (2014) Exploring the usefulness of two variants of gaze-guiding-based dynamic job aid for performing a fixed sequence start up procedure after longer periods of non-use. Hum Fact Ergon 3(2):148\u2013169","journal-title":"Hum Fact Ergon"},{"key":"1_CR107","unstructured":"Knight JC, Kienzle DM (1992) Preliminary experience Using Z to specify a Safety-critical system. In: Proceedings of Z User workshop, pp 109\u2013118"},{"key":"1_CR108","doi-asserted-by":"crossref","unstructured":"Knight JC, Brilliant SS (1997) Preliminary evaluation of a formal approach to user interface specification. In: The Z formal specification notation. Springer, pp 329\u2013346","DOI":"10.1007\/BFb0027296"},{"key":"1_CR109","doi-asserted-by":"crossref","unstructured":"Knight JC, Fletcher PT, Hicks BR (1999) Tool support for production use of formal techniques. In: Proceedings of the world congress on formal methods in the development of computing systems, pp 242\u2013251","DOI":"10.1007\/3-540-48118-4_48"},{"key":"1_CR110","unstructured":"Kummer O, Wienberg F, Duvigneau M, K\u00f6hler M, Moldt D, R\u00f6lke H (2000) Renew\u2013the reference net workshop. In: Proceedings of 21st international conference on application and theory of petri nets-tool demonstrations, pp 87\u201389"},{"key":"1_CR111","volume-title":"Referenznetze","author":"O Kummer","year":"2002","unstructured":"Kummer O (2002) Referenznetze. Universit\u00e4t Hamburg, Disseration"},{"key":"1_CR112","doi-asserted-by":"crossref","unstructured":"Li K-Y, Oladimeji P, Thimbleby HW (2015) Exploring the effect of pre-operational priming intervention on number entry errors. In: Proceedings of the 33rd annual ACM conference on human factors in computing systems, pp 1335\u20131344","DOI":"10.1145\/2702123.2702477"},{"key":"1_CR113","doi-asserted-by":"crossref","unstructured":"Loer K, Harrison MD (2000) formal interactive systems analysis and usability inspection methods: two incompatible worlds? In: Interactive systems: design, specification, and verification, pp 169\u2013190","DOI":"10.1007\/3-540-44675-3_11"},{"key":"1_CR114","doi-asserted-by":"crossref","unstructured":"Loer K, Harrison MD (2002) Towards usable and relevant model checking techniques for the analysis of dependable interactive systems. In: Proceedings of automated software engineering, pp 223\u2013226","DOI":"10.1109\/ASE.2002.1115016"},{"issue":"4","key":"1_CR115","doi-asserted-by":"crossref","first-page":"469","DOI":"10.1007\/s10515-006-7999-y","volume":"13","author":"K Loer","year":"2006","unstructured":"Loer K, Harrison MD (2006) An integrated framework for the analysis of dependable interactive systems (IFADIS): its tool support and evaluation. Autom Softw Eng 13(4):469\u2013496","journal-title":"Autom Softw Eng"},{"key":"1_CR116","doi-asserted-by":"crossref","unstructured":"Lutz RR (2000) Software engineering for safety: a roadmap. In: Proceedings of the conference on the future of software engineering, pp 213\u2013226","DOI":"10.1145\/336512.336556"},{"key":"1_CR117","doi-asserted-by":"crossref","unstructured":"Mancini R (1997) Modelling interactive computing by exploiting the undo. Dissertation, University of Rome","DOI":"10.1007\/978-0-387-35175-9_140"},{"key":"1_CR118","doi-asserted-by":"crossref","unstructured":"Markopoulos P (1995) On the expression of interaction properties within an interactor model. In: Interactive systems: design, specification, and verification, pp 294\u2013310","DOI":"10.1007\/978-3-7091-9437-9_18"},{"key":"1_CR119","unstructured":"Markopoulos P, Rowson J, Johnson P (1996) Dialogue modelling in the framework of an interactor model. In: Pre-conference proceedings of design specification and verification of interactive systems, Namur, Belgium, vol 44"},{"key":"1_CR120","unstructured":"Markopoulos P (1997) A compositional model for the formal specification of user interface software. Dissertation, University of London"},{"issue":"5","key":"1_CR121","doi-asserted-by":"crossref","first-page":"675","DOI":"10.1006\/ijhc.1998.0223","volume":"49","author":"P Markopoulos","year":"1998","unstructured":"Markopoulos P, Johnson P, Rowson J (1998) Formal architectural abstractions for interactive software. Int J Hum Comput Stud 49(5):675\u2013715","journal-title":"Int J Hum Comput Stud"},{"key":"1_CR122","doi-asserted-by":"crossref","unstructured":"Martinie C, Palanque PA, Navarre D, Winckler M, Poupart E (2011) Model-based training: an approach supporting operability of critical interactive systems. In: Proceedings of ACM EICS conference, pp 53\u201362","DOI":"10.1145\/1996461.1996495"},{"key":"1_CR123","doi-asserted-by":"crossref","unstructured":"Martinie C, Palanque PA, Winckler M (2011) Structuring and composition mechanisms to address scalability issues in task models. In: Proceedings of IFIP TC 13 INTERACT, pp 589\u2013609","DOI":"10.1007\/978-3-642-23765-2_40"},{"issue":"1","key":"1_CR124","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/j.ijhcs.2013.08.013","volume":"72","author":"C Martinie","year":"2014","unstructured":"Martinie C, Navarre D, Palanque PA (2014) A multi-formalism approach for model-based dynamic distribution of user interfaces of critical interactive systems. Int J Hum Comput Stud 72(1):77\u201399","journal-title":"Int J Hum Comput Stud"},{"key":"1_CR125","unstructured":"Masci P, Ruksenas R, Oladimeji P, Cauchi A, Gimblett A, Li Y, Curzon P, Thimbleby H (2011) On formalising interactive number entry on infusion pumps. Electron Commun the EASST 45"},{"key":"1_CR126","doi-asserted-by":"crossref","unstructured":"Masci P, Ayoub A, Curzon P, Harrison MD, Lee I, Thimbleby H (2013a) Verification of interactive software for medical devices: PCA infusion pumps and FDA regulation as an example. In: Proceedings of the 5th ACM SIGCHI symposium on engineering interactive computing systems pp 81\u201390","DOI":"10.1145\/2494603.2480302"},{"key":"1_CR127","doi-asserted-by":"crossref","unstructured":"Masci P, Zhang Y, Jones PL, Oladimeji P, D\u2019Urso E, Bernardeschi C, Curzon P, Thimbleby H (2014a) Formal verification of medical device user interfaces using PVS. In: Proceedings of the 17th international conference on fundamental approaches to software engineering. Springer, pp 200\u2013214","DOI":"10.1007\/978-3-642-54804-8_14"},{"key":"1_CR128","doi-asserted-by":"crossref","unstructured":"Masci P, Zhang Y, Jones PL, Oladimeji P, D\u2019Urso E, Bernardeschi C, Curzon P, Thimbleby H (2014b) Combining PVSio with stateflow. In: Proceedings of NASA formal methods\u20146th international symposium, pp 209\u2013214","DOI":"10.1007\/978-3-319-06200-6_16"},{"issue":"2","key":"1_CR129","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1007\/s11334-013-0200-4","volume":"11","author":"P Masci","year":"2015","unstructured":"Masci P, Ruksenas R, Oladimeji P, Cauchi A, Gimblett A, Li AY, Curzon P, Thimbleby HW (2015) The benefits of formalising design guidelines: a case study on the predictability of drug infusion pumps. Innov Syst Softw Eng 11(2):73\u201393","journal-title":"Innov Syst Softw Eng"},{"key":"1_CR130","doi-asserted-by":"crossref","unstructured":"Mateescu R, Thivolle D (2008) A model checking language for concurrent value-passing systems. In: Cuellar J, Maibaum T, Sere K (eds) Proceedings of the 15th international symposium on formal methods. Springer, pp 148\u2013164","DOI":"10.1007\/978-3-540-68237-0_12"},{"key":"1_CR131","doi-asserted-by":"crossref","unstructured":"Merriam NA, Harrison MD (1996) Evaluating the interfaces of three theorem proving assistants. In: Proceedings of DSV-IS conference. Springer, pp 330\u2013346","DOI":"10.1007\/978-3-7091-7491-3_17"},{"issue":"4\u20135","key":"1_CR132","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1007\/s10009-004-0173-6","volume":"8","author":"SP Miller","year":"2006","unstructured":"Miller SP, Tribble AC, Whalen MW, Heimdahl MPE (2006) Proving the shalls. Int J Softw Tools Technol Transf 8(4\u20135):303\u2013319","journal-title":"Int J Softw Tools Technol Transf"},{"key":"1_CR133","doi-asserted-by":"crossref","unstructured":"Miller SP (2009) Bridging the gap between model-based development and model checking. In: Tools and algorithms for the construction and analysis of systems. Springer, pp 443\u2013453","DOI":"10.1007\/978-3-642-00768-2_36"},{"issue":"2","key":"1_CR134","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1145\/1646353.1646372","volume":"53","author":"SP Miller","year":"2010","unstructured":"Miller SP, Whalen MW, Cofer DD (2010) Software model checking takes off. Commun ACM 53(2):58\u201364","journal-title":"Commun ACM"},{"key":"1_CR135","doi-asserted-by":"crossref","unstructured":"Milner R (1980) A calculus of communicating systems. Springer","DOI":"10.1007\/3-540-10235-3"},{"key":"1_CR136","unstructured":"Moher T, Dirda V, Bastide R (1996) A bridging framework for the modelling of devices, users, and interfaces. Technical report"},{"key":"1_CR137","doi-asserted-by":"crossref","unstructured":"Murugesan A, Whalen MW, Rayadurgam S, Heimdahl MPE (2013) Compositional verification of a medical device system. In: Proceedings of the 2013 ACM SIGAda annual conference on high integrity language technology, pp 51\u201364","DOI":"10.1145\/2527269.2527272"},{"key":"1_CR138","doi-asserted-by":"crossref","unstructured":"Navarre D, Palanque PA, Paterno F, Santoro C, Bastide R (2001) A tool suite for integrating task and system models through scenarios. In: Proceedings of the 8th international workshop on interactive systems: design, specification, and verification-revised papers. Springer, pp 88\u2013113","DOI":"10.1007\/3-540-45522-1_6"},{"key":"1_CR139","doi-asserted-by":"crossref","unstructured":"Navarre D, Palanque PA, Bastide R, Schyn A, Winckler M, Nedel LP, Freitas CMDS (2005) A formal description of multimodal interaction techniques for immersive virtual reality applications. In: Proceedings of the 2005 IFIP TC13 international conference on human-computer interaction. Springer, pp 170\u2013183","DOI":"10.1007\/11555261_17"},{"key":"1_CR140","doi-asserted-by":"crossref","unstructured":"Navarre D, Palanque PA, Basnyat S (2008) A formal approach for user interaction reconfiguration of safety critical interactive systems. In: Computer safety, reliability, and security. Springer, pp 373\u2013386","DOI":"10.1007\/978-3-540-87698-4_31"},{"issue":"4","key":"1_CR141","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1614390.1614393","volume":"16","author":"D Navarre","year":"2009","unstructured":"Navarre D, Palanque PA, Ladry J-F, Barboni E (2009) ICOs: a model-based user interface description technique dedicated to interactive systems addressing usability, reliability and scalability. ACM Trans Comput Hum Interact 16(4):1\u201356","journal-title":"ACM Trans Comput Hum Interact"},{"issue":"3","key":"1_CR142","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/PL00011531","volume":"3","author":"Y Niwa","year":"2001","unstructured":"Niwa Y, Takahashi M, Kitamura M (2001) The design of human-machine interface for accident support in nuclear power plants. Cogn Technol Work 3(3):161\u2013176","journal-title":"Cogn Technol Work"},{"key":"1_CR143","doi-asserted-by":"crossref","unstructured":"Oladimeji P, Thimbleby HW, Cox AL (2011) number entry interfaces and their effects on error detection. In: Proceedings of human-computer interaction\u2014INTERACT 2011\u201413th IFIP TC 13 international conference, pp 178\u2013185","DOI":"10.1007\/978-3-642-23768-3_15"},{"key":"1_CR144","doi-asserted-by":"crossref","unstructured":"Oladimeji P, Thimbleby HW, Cox AL (2013) A performance review of number entry interfaces. In: Proceedings of human-computer interaction\u2014INTERACT 2013\u201414th IFIP TC 13 international conference, pp 365\u2013382","DOI":"10.1007\/978-3-642-40483-2_26"},{"key":"1_CR145","doi-asserted-by":"crossref","unstructured":"Oliveira R, Dupuy-Chessa S, Calvary G (2014) Formal verification of UI using the power of a recent tool suite. In: Proceedings of the ACM SIGCHI symposium on engineering interactive computing systems, pp 235\u2013240","DOI":"10.1145\/2607023.2610280"},{"key":"1_CR146","unstructured":"Oliveira R (2015) Formal specification and verification of interactive systems with plasticity: applications to nuclear-plant supervision. Dissertation, Universit\u00e9 Grenoble Alpes"},{"issue":"3","key":"1_CR147","doi-asserted-by":"crossref","first-page":"192","DOI":"10.1515\/icom-2015-0036","volume":"14","author":"R Oliveira","year":"2015","unstructured":"Oliveira R, Dupuy-Chessa S, Calvary G (2015a) Verification of plastic interactive systems. i-com 14(3):192\u2013204","journal-title":"i-com"},{"key":"1_CR148","doi-asserted-by":"crossref","unstructured":"Oliveira R, Dupuy-Chessa S, Calvary G (2015b) Equivalence checking for comparing user interfaces. In: Proceedings of the 7th ACM SIGCHI Symposium on Engineering Interactive Computing Systems, p 266\u2013275","DOI":"10.1145\/2774225.2774844"},{"key":"1_CR149","doi-asserted-by":"crossref","unstructured":"Oliveira R, Dupuy-Chessa S, Calvary G (2015c) Plasticity of user interfaces: formal verification of consistency. In: Proceedings of the 7th ACM SIGCHI symposium on engineering interactive computing systems, pp 260\u2013265","DOI":"10.1145\/2774225.2775078"},{"key":"1_CR150","unstructured":"OMG (2010) Systems modelling language (OMG SysML\u2122), version 1.2"},{"key":"1_CR151","unstructured":"Palanque PA, Bastide R, Seng\u00e8s V (1995) Validating interactive system design through the verification of formal task and system models. In: Proceedings of IFIP WG 2.7 conference on engineering human computer interaction, pp 189\u2013212"},{"key":"1_CR152","doi-asserted-by":"crossref","unstructured":"Palanque PA, Bastide R (1995) Petri net based design of user-driven interfaces using the interactive cooperative objects formalism. In: Interactive systems: design, specification, and verification. Springer, pp 383\u2013400","DOI":"10.1007\/978-3-642-87115-3_23"},{"key":"1_CR153","doi-asserted-by":"crossref","unstructured":"Palanque PA, Bastide R, Senges V (1996) Validating interactive system design through the verification of formal task and system models. In: Proceedings of the IFIP TC2\/WG2.7 working conference on engineering for human-computer interaction, pp 189\u2013212","DOI":"10.1007\/978-0-387-34907-7_11"},{"key":"1_CR154","unstructured":"Palanque PA, Patern\u00f3 F (eds) (1997) Formal methods in HCI. Springer"},{"key":"1_CR155","doi-asserted-by":"crossref","unstructured":"Palanque PA, Bastide R, Patern\u00f3 F (1997) Formal specification as a tool for objective assessment of safety-critical interactive systems. In: Proceedings of the IFIP TC13 international conference on human-computer interaction, pp 323\u2013330","DOI":"10.1007\/978-0-387-35175-9_53"},{"key":"1_CR156","unstructured":"Palanque PA, Farenc C, Bastide R (1999) Embedding ergonomic rules as generic requirements in a formal development process of interactive software. In: Human-computer interaction INTERACT\u201999: IFIP TC13 international conference on human-computer interaction, pp 408\u2013416"},{"key":"1_CR157","doi-asserted-by":"crossref","unstructured":"Palanque PA, Winckler M, Ladry J-F, ter Beek M, Faconti G, Massink M (2009) A formal approach supporting the comparative predictive assessment of the interruption-tolerance of interactive systems. In: Proceedings of ACM EICS 2009 conference, pp 46\u201355","DOI":"10.1145\/1570433.1570473"},{"issue":"2","key":"1_CR158","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1207\/s15327051hci0202_1","volume":"2","author":"SJ Payne","year":"1986","unstructured":"Payne SJ, Green TRG (1986) Task-action grammars: a model of mental representation of task languages. Hum Comput Interact 2(2):93\u2013133","journal-title":"Hum Comput Interact"},{"key":"1_CR159","doi-asserted-by":"crossref","unstructured":"Park D (1981) Concurrency and automata on infinite sequences. In: Proceedings of the 5th GI-conference on theoretical computer science. Springer, pp 167\u2013183","DOI":"10.1007\/BFb0017309"},{"key":"1_CR160","doi-asserted-by":"crossref","unstructured":"Parnas DL (1969) On the use of transition diagrams in the design of a user interface for an interactive computer system. In: Proceedings of the 24th national ACM conference, pp 379\u2013385","DOI":"10.1145\/800195.805945"},{"key":"1_CR161","unstructured":"Patern\u00f3 F, Faconti G (1992) On the use of LOTOS to describe graphical interaction. People and computers VII. Cambridge University Press, pp 155\u2013155"},{"issue":"3","key":"1_CR162","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1006\/jvlc.1994.1012","volume":"5","author":"F Patern\u00f3","year":"1994","unstructured":"Patern\u00f3 F (1994) A Theory of User-interaction Objects. J Vis Lang Comput 5(3):227\u2013249","journal-title":"J Vis Lang Comput"},{"key":"1_CR163","unstructured":"Patern\u00f3 F, Mezzanotte M (1994) Analysing MATIS by interactors and ACTL. Technical report"},{"key":"1_CR164","doi-asserted-by":"crossref","unstructured":"Patern\u00f3 F, Mezzanotte M (1996) Formal verification of undesired behaviours in the CERD case study. In: Proceedings of the IFIP TC2\/WG2.7 working conference on engineering for human-computer interaction, pp 213\u2013226","DOI":"10.1007\/978-0-387-34907-7_12"},{"issue":"2","key":"1_CR165","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1016\/S0953-5438(97)00015-5","volume":"9","author":"F Patern\u00f3","year":"1997","unstructured":"Patern\u00f3 F (1997) Formal reasoning about dialogue properties with automatic support. Interact Comput 9(2):173\u2013196","journal-title":"Interact Comput"},{"key":"1_CR166","doi-asserted-by":"crossref","unstructured":"Patern\u00f3 F, Mancini C, Meniconi S (1997) ConcurTaskTrees: a diagrammatic notation for specifying task models. In: Proceedings of the IFIP tc13 international conference on human-computer interaction, pp 362\u2013369","DOI":"10.1007\/978-0-387-35175-9_58"},{"key":"1_CR167","doi-asserted-by":"crossref","unstructured":"Patern\u00f3 F, Santoro C (2001). Integrating Model checking and HCI tools to help designers verify user interface properties. In: Proceedings of the 7th international conference on design, specification, and verification of interactive systems. Springer, pp 135\u2013150","DOI":"10.1007\/3-540-44675-3_9"},{"issue":"4","key":"1_CR168","doi-asserted-by":"crossref","first-page":"340","DOI":"10.1093\/comjnl\/46.4.340","volume":"46","author":"F Patern\u00f3","year":"2003","unstructured":"Patern\u00f3 F, Santoro C (2003) Support for reasoning about interactive systems through human-computer interaction designers\u2019 representations. Comput J 46(4):340\u2013357","journal-title":"Comput J"},{"key":"1_CR52","unstructured":"Petri CA (1962) Kommunikation mit Automaten. Dissertation, University of Bonn"},{"volume-title":"Seeheim workshop on user interface management systems","year":"1985","key":"1_CR169","unstructured":"Pfaff G, Hagen P (eds) (1985) Seeheim workshop on user interface management systems. Springer, Berlin"},{"key":"1_CR170","doi-asserted-by":"crossref","unstructured":"Reeve G, Reeves S (2000) \u03bcCharts and Z: Hows, Whys, and Wherefores. In: Integrated formal methods: second international conference. Springer, Berlin","DOI":"10.1007\/3-540-40911-4_15"},{"issue":"2","key":"1_CR171","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1109\/TSE.1981.234520","volume":"7","author":"P Reisner","year":"1981","unstructured":"Reisner P (1981) Formal grammar and human factors design of an interactive graphics system. IEEE Trans Softw Eng 7(2):229\u2013240","journal-title":"IEEE Trans Softw Eng"},{"key":"1_CR172","doi-asserted-by":"crossref","unstructured":"Schwaber K (2004) Agile project management with scrum. Microsoft Press","DOI":"10.1007\/11499053_47"},{"key":"1_CR173","unstructured":"Sifakis J (1979) Use of petri nets for performance evaluation. In: Beilner H, Gelenbe E (eds), Proceedings of 3rd international symposium on modelling and performance of computer systems"},{"key":"1_CR174","unstructured":"Shepherd A (1989) Analysis and training in information technology tasks. In Diaper D (ed) Task analysis for human-computer interaction, pp 15\u201355"},{"key":"1_CR175","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1016\/0167-6423(82)90014-4","volume":"1","author":"B Sufrin","year":"1982","unstructured":"Sufrin B (1982) Formal specification of a display-oriented text editor. Sci Comput Program 1:157\u2013202","journal-title":"Sci Comput Program"},{"key":"1_CR176","unstructured":"Sousa M, Campos J, Alves M, Harrison M, (2014) Formal verification of safety-critical user interfaces: a space system case study. In: Proceedings of the AAAI spring symposium on formal verification and modelling in human machine systems, pp 62\u201367"},{"key":"1_CR177","volume-title":"The Z notation: a reference manual","author":"MJ Spivey","year":"1989","unstructured":"Spivey MJ (1989) The Z notation: a reference manual. Prentice-Hall, Upper Saddle River"},{"key":"1_CR178","doi-asserted-by":"crossref","unstructured":"Strunk EA, Yin X, Knight JC (2005) ECHO: a practical approach to formal verification. In: Proceedings of the 10th international workshop on formal methods for industrial critical systems, pp 44\u201353","DOI":"10.1145\/1081180.1081187"},{"key":"1_CR179","unstructured":"St\u00fcckrath J, Weyers, B (2014) Lattice-extended coloured petri net rewriting for adaptable user interface models. Electron Commun EASST 67(13):13 pages. http:\/\/journal.ub.tu-berlin.de\/eceasst\/article\/view\/941\/929"},{"key":"1_CR180","unstructured":"Thevenin D, Coutaz J (1999) Plasticity of user interfaces: framework and research agenda. In: Sasse A, Johnson C (eds) Proceedings of interact, pp 110\u2013117"},{"key":"1_CR181","doi-asserted-by":"crossref","unstructured":"Thimbleby H (2007a) Interaction walkthrough: evaluation of safety critical interactive systems. In: interactive systems. design, specification, and verification. Springer, pp 52\u201366","DOI":"10.1007\/978-3-540-69554-7_5"},{"key":"1_CR182","doi-asserted-by":"crossref","unstructured":"Thimbleby H (2007b) User-centered methods are insufficient for safety critical systems. In: Proceedings of the 3rd human-computer interaction and usability engineering of the austrian computer society conference on HCI and usability for medicine and health care. Springer, pp 1\u201320","DOI":"10.1007\/978-3-540-76805-0_1"},{"key":"1_CR183","doi-asserted-by":"crossref","unstructured":"Thimbleby H, Gow J (2008) Applying graph theory to interaction design. In: Gulliksen J, Harning MB, Palanque P, Veer GC, Wesson J (eds) Engineering interactive systems. Springer, pp 501\u2013519","DOI":"10.1007\/978-3-540-92698-6_30"},{"issue":"4","key":"1_CR184","doi-asserted-by":"crossref","first-page":"349","DOI":"10.2498\/cit.1001921","volume":"18","author":"H Thimbleby","year":"2010","unstructured":"Thimbleby H (2010) Think! interactive systems need safety locks. J Comput Inf Technol 18(4):349\u2013360","journal-title":"J Comput Inf Technol"},{"key":"1_CR185","unstructured":"Thimbleby HW, Gimblett A (2011) Dependable keyed data entry for interactive systems. Electron Commun EASST 45"},{"key":"1_CR186","doi-asserted-by":"crossref","unstructured":"Tu H, Oladimeji P, Li KY, Thimbleby HW, Vincent C (2014) The effects of number-related factors on entry performance. In: Proceedings of the 28th international BCS human computer interaction conference, pp 246\u2013251","DOI":"10.14236\/ewic\/hci2014.31"},{"key":"1_CR187","unstructured":"Turchin P, Skii R (2006) History and mathematics. URSS"},{"key":"1_CR188","unstructured":"Turner CS (1993) An investigation of the therac-25 accidents. Computer 18:9I62\/93, 0700\u2013001830300"},{"issue":"3","key":"1_CR189","doi-asserted-by":"crossref","first-page":"555","DOI":"10.1145\/233551.233556","volume":"43","author":"RJ Glabbeek van","year":"1996","unstructured":"van Glabbeek RJ, Weijland WP (1996) Branching time and abstraction in bisimulation semantics. J ACM 43(3):555\u2013600","journal-title":"J ACM"},{"key":"1_CR190","doi-asserted-by":"crossref","unstructured":"Wang H-W, Abowd G (1994) A tabular interface for automated verification of event-based dialogs. Technical report. DTIC Document","DOI":"10.21236\/ADA286065"},{"issue":"5","key":"1_CR191","doi-asserted-by":"crossref","first-page":"80","DOI":"10.1145\/253769.253801","volume":"40","author":"P Wegner","year":"1997","unstructured":"Wegner P (1997) Why interaction is more powerful than algorithms. Commun ACM 40(5):80\u201391","journal-title":"Commun ACM"},{"key":"1_CR192","doi-asserted-by":"crossref","unstructured":"Weyers B, Baloian N, Luther W (2009) Cooperative creation of concept keyboards in distributed learning environments. In: Borges MRS, Shen W, Pino JA, Barth\u00e8s J-P, Lou J, Ochoa SF, Yong J (eds), Proceedings of 13th international conference on CSCW in design, pp 534\u2013539","DOI":"10.1109\/CSCWD.2009.4968114"},{"issue":"1","key":"1_CR193","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1016\/j.future.2010.05.001","volume":"27","author":"B Weyers","year":"2010","unstructured":"Weyers B, Luther W, Baloian N (2010a) Interface creation and redesign techniques in collaborative learning scenarios. J Futur Gener Comput Syst 27(1):127\u2013138","journal-title":"J Futur Gener Comput Syst"},{"key":"1_CR194","doi-asserted-by":"crossref","unstructured":"Weyers B, Burkolter D, Kluge A, Luther W (2010) User-centered interface reconfiguration for error reduction in human-computer interaction. In: Proceedings of the third international conference on advances in human-oriented and personalized mechanisms, technologies and services, pp 52\u201355","DOI":"10.1109\/CENTRIC.2010.11"},{"issue":"6","key":"1_CR195","doi-asserted-by":"crossref","first-page":"1127","DOI":"10.1142\/S0219622012400172","volume":"11","author":"B Weyers","year":"2012","unstructured":"Weyers B, Luther W, Baloian N (2012a) Cooperative reconfiguration of user interfaces for learning cryptographic algorithms. J Inf Technol Decis Mak 11(6):1127\u20131154","journal-title":"J Inf Technol Decis Mak"},{"key":"1_CR196","unstructured":"Weyers B (2012) Reconfiguration of user interface models for monitoring and control of human-computer systems. Dissertation, University of Duisburg-Essen. Dr. Hut, Berlin"},{"issue":"1","key":"1_CR197","doi-asserted-by":"crossref","first-page":"646","DOI":"10.1080\/10447318.2011.654199","volume":"28","author":"B Weyers","year":"2012","unstructured":"Weyers B, Burkolter D, Luther W, Kluge A (2012b) Formal modelling and reconfiguration of user interfaces for reduction of human error in failure handling of complex systems. J Hum Comput Interact 28(1):646\u2013665","journal-title":"J Hum Comput Interact"},{"issue":"1&2","key":"1_CR198","first-page":"302","volume":"7","author":"B Weyers","year":"2014","unstructured":"Weyers B, Borisov N, Luther W (2014) Creation of adaptive user interfaces through reconfiguration of user interface models using an algorithmic rule generation approach. Int J Adv Intell Syst 7(1&2):302\u2013336","journal-title":"Int J Adv Intell Syst"},{"key":"1_CR199","unstructured":"Weyers B (2015) FILL: formal description of executable and reconfigurable models of interactive systems. In: Proceedings of the workshop on formal methods in human computer interaction, pp 1\u20136"},{"issue":"2","key":"1_CR200","doi-asserted-by":"crossref","first-page":"59","DOI":"10.4018\/IJISCRAM.2015040104","volume":"7","author":"B Weyers","year":"2015","unstructured":"Weyers B, Frank B, Bischof K, Kluge A (2015) Gaze guiding as support for the control of technical systems. Int J Inf Syst Crisis Resp Manag 7(2):59\u201380","journal-title":"Int J Inf Syst Crisis Resp Manag"},{"key":"1_CR201","doi-asserted-by":"crossref","unstructured":"Whalen M, Cofer D, Miller S, Krogh BH, Storm W (2008) Integration of formal analysis into a model-based software development process. In: Formal methods for industrial critical systems. Springer, pp 68\u201384","DOI":"10.1007\/978-3-540-79707-4_7"},{"key":"1_CR202","doi-asserted-by":"crossref","unstructured":"Yin X, Knight JC, Nguyen EA, Weimer W (2008) Formal verification by reverse synthesis. In: Proceedings of international conference on computer safety, reliability, and security, pp 305\u2013319","DOI":"10.1007\/978-3-540-87698-4_26"},{"key":"1_CR203","doi-asserted-by":"crossref","unstructured":"Yin X, Knight J, Weimer W (2009a) Exploiting refactoring in formal verification. In: Proceedings of dependable systems & networks, pp 53\u201362","DOI":"10.1109\/DSN.2009.5270355"},{"key":"1_CR204","doi-asserted-by":"crossref","unstructured":"Yin X, Knight JC, Weimer W (2009b) Exploiting refactoring in formal verification. In: Proceedings of the 2009 IEEE\/IFIP international conference on dependable systems and networks, pp 53\u201362","DOI":"10.1109\/DSN.2009.5270355"},{"key":"1_CR205","unstructured":"Yin X, Knight JC (2010) Formal verification of large software systems. In: Proceedings of second NASA formal methods symposium, pp 192\u2013201"}],"container-title":["Human\u2013Computer Interaction Series","The Handbook of Formal Methods in Human-Computer Interaction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-51838-1_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,23]],"date-time":"2024-06-23T18:50:12Z","timestamp":1719168612000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-51838-1_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319518374","9783319518381"],"references-count":205,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-51838-1_1","relation":{},"ISSN":["1571-5035"],"issn-type":[{"type":"print","value":"1571-5035"}],"subject":[],"published":{"date-parts":[[2017]]}}}