. Abowd, Structuring the Space of Interactive System Properties, Proceedings of the IFIP TC2/WG2.7 Working Conference on Engineering for Human-Computer Interaction, pp.113-129, 1992.

. Abowd, A formal technique for automated dialogue development, Proceedings of the conference on Designing interactive systems processes, practices, methods, & techniques, DIS '95, pp.219-226, 1995.
DOI : 10.1145/225434.225459

D. Gregory and . Abowd, Formal Aspects of Human-computer Interaction, 1991.

]. Abrial, The B-book: Assigning Programs to Meanings, 1996.
DOI : 10.1017/CBO9780511624162

]. Abrial, Formal methods in industry, Proceeding of the 28th international conference on Software engineering , ICSE '06, pp.761-768, 2006.
DOI : 10.1145/1134285.1134406

. Acharya, Human Computer Interaction and Medical Devices, Proceedings of the 2010 British Computer Society Conference on Human-Computer Interaction, BCS-HCI 2010, pp.6-10, 2010.

&. Aït-ameur and . Baron, Formal and experimental validation approaches in HCI systems design based on a shared event B model, International Journal on Software Tools for Technology Transfer, vol.8, issue.3, pp.547-563, 2006.
DOI : 10.1007/s10009-006-0008-8

&. Aït-ameur and . Kamel, Yamine Aït-Ameur et Nadjet Kamel. A Generic Formal Specification of Fusion of Modalities in a Multimodal HCI, Building the Information Society, pp.415-420, 2004.

. Aït-ameur, A Uniform Approach for Specification and Design of Interactive Systems: the B Method, Design, Specification and Verification of Interactive Systems'98, Supplementary Proceedings of the Fifth International Eurographics Workshop, pp.51-67, 1998.

. Aït-ameur, A Uniform Approach for the Specification and Design of Interactive Systems: The B Method, Eurographics Workshop on Design, Specification, and Verification of Interactive Systems (DSVIS'98) Proceedings (Eds, Markopoulos, P. and Johnson, pp.333-352, 1998.

. Aït-ameur, Using the B formal approach for incremental specification design of interactive systems, Engineering for Human-Computer Interaction, pp.91-109, 1999.
DOI : 10.1007/978-0-387-35349-4_6

. Aït-ameur, Formal Validation of HCI User Tasks, Software Engineering Research and Practice, pp.732-738, 2003.

. Aït-ameur, Utilisation de Techniques Formelles dans la Modélisation d'Interfaces Homme-machine. Une Expérience Comparative entre B et Promela/SPIN, 6th International Symposium on Programming and Systems ISPS, pp.57-66, 2003.

. Aït-ameur, Formal Verification and Validation of Interactive Systems Specifications, Human Error, Safety and Systems Development, pp.61-76, 2004.
DOI : 10.1007/1-4020-8153-7_5

. Aït-ameur, Encoding a Process Algebra Using the Event B Method. Application to the Validation of User Interfaces, Proceedings of 2nd IEEE international symposium on leveraging applications of formal methods (ISOLA), 2005.

. Aït-ameur, Validation et v??rification formelles de syst??mes interactifs multi-modaux fond??es sur la preuve, Proceedings of the 18th international conference on Association Francophone d'Interaction Homme-Machine , IHM '06, pp.123-130, 2006.
DOI : 10.1145/1132736.1132752

. Aït-ameur, Vérification et Validation Formelles de Systèmes Interactifs Fondées sur la Preuve: Application aux Systèmes Multi-Modaux, Journal d'Interaction Personne-Systéme (JIPS), pp.1-30, 2010.

. Aït-ameur, On Implicit and Explicit Semantics: Integration Issues in Proof-Based Development of Systems, Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications, pp.604-618, 2014.
DOI : 10.1007/978-3-662-45231-8_50

&. Aït-sadoune and . Aït-ameur, Idir Aït-Sadoune et Yamine Aït-Ameur Animating Event B Models by Formal Data Models, Leveraging Applications of Formal Methods, Verification and Validation, Third International Symposium. Proceedings, pp.37-55, 2008.

. Ameur, Toward a wider use of formal methods for aerospace systems design and verification, International Journal on Software Tools for Technology Transfer, vol.221, issue.2, pp.1-7, 2010.
DOI : 10.1007/s10009-009-0131-4

&. Baecker, . Buxton, M. Ronald, . Baecker, A. William et al., Readings in Humancomputer Interaction, 2014.

. Bass, The ARCH model: Seeheim Revisited, User Interface Developpers' Workshop, 1991.

&. Bastide and . Palanque, Rémi Bastide et Philippe A Palanque. Petri Net Objects for the Design, Validation and Prototyping of User-driven Interfaces, Interact, pp.625-631, 1990.

&. Bastide and . Palanque, Rémi Bastide et Philippe Palanque A Petri Net based Environment for the Design of Event-driven Interfaces. In Application and Theory of Petri Nets, pp.66-83, 1995.

]. Bastide, D. Navarre, and P. Palanque, A tool-supported design framework for safety critical interactive systems, Interacting with Computers, vol.15, issue.3, pp.309-328, 2003.
DOI : 10.1016/S0953-5438(03)00011-0

]. Bastide, D. Navarre, P. A. Palanque, A. Schyn, and P. Dragicevic, A model-based approach for real-time embedded multimodal systems in military aircrafts, Proceedings of the 6th international conference on Multimodal interfaces , ICMI '04, pp.243-250, 2004.
DOI : 10.1145/1027933.1027974

&. Bastien, ]. J. Scapin, D. L. Christian-bastien, and . Scapin, A validation of ergonomic criteria for the evaluation of human???computer interfaces, International Journal of Human-Computer Interaction, vol.1, issue.2, 1993.
DOI : 10.1080/10447319009525981

S. Bauersfeld, E. J. Tanja, and . Vos, GUITest: a Java library for fully automated GUI robustness testing, Proceedings of the 27th IEEE/ACM International Conference on Automated Software Engineering, ASE 2012, pp.330-333, 2012.
DOI : 10.1145/2351676.2351739

S. Bauersfeld, E. J. Tanja, and . Vos, User Interface Level Testing with TESTAR; What about More Sophisticated Action Specification and Selection? In Post-proceedings of the Seventh Seminar on Advanced Techniques and Tools for Software Evolution, pp.9-11, 2014.

. Bauersfeld, A Metaheuristic Approach to Test Sequence Generation for Applications with a GUI, Search Based Software Engineering -Third International Symposium, SSBSE 2011. Proceedings, pp.173-187, 2011.
DOI : 10.1002/stvr.294

. Bauersfeld, An approach to automatic input sequence generation for GUI testing using ant colony optimization, Proceedings of the 13th annual conference companion on Genetic and evolutionary computation, GECCO '11, pp.251-252, 2011.
DOI : 10.1145/2001858.2001999

. Bauersfeld, Evaluating rogue user testing in industry: An experience report, 2014 IEEE Eighth International Conference on Research Challenges in Information Science (RCIS), pp.1-10, 2014.
DOI : 10.1109/RCIS.2014.6861051

. Bauersfeld, Evaluating the TESTAR tool in an industrial case study, Proceedings of the 8th ACM/IEEE International Symposium on Empirical Software Engineering and Measurement, ESEM '14, pp.1-49, 2014.
DOI : 10.1145/2652524.2652588

]. Bauersfeld, GUIdiff -- A Regression Testing Tool for Graphical User Interfaces, 2013 IEEE Sixth International Conference on Software Testing, Verification and Validation, pp.499-500, 2013.
DOI : 10.1109/ICST.2013.84

. Bertino, Design issues in interactive user interfaces, Interfaces in Computing, vol.3, issue.1, pp.37-53, 1985.
DOI : 10.1016/0252-7308(85)90020-0

. Bhasin, Orthogonal Testing Using Genetic Algorithms, International Journal of Computer Science and Information Technology, vol.4, issue.2, pp.374-377, 2013.

L. Matthew and . Bolton, Modeling Human Perception Could Stevens' Power Law Be an Emergent Feature? In SMC, pp.1073-1078, 2008.

. Booch, Unified Modeling Language User Guide, The, 2005.

A. Paul and . Booth, An Introduction to Human-computer Interaction, 1989.

&. Borjesson, . Feldt, R. Borjesson, and . Feldt, Automated System Testing Using Visual GUI Testing Tools: A Comparative Study in Industry, 2012 IEEE Fifth International Conference on Software Testing, Verification and Validation, pp.350-359, 2012.
DOI : 10.1109/ICST.2012.115

. Bouajjani, Safety for branching time semantics, Automata, Languages and Programming, pp.76-92, 1991.
DOI : 10.1007/3-540-54233-7_126

J. Bowen and S. Reeves, Including Design Guidelines in the Formal Specification of Interfaces in Z, ZB 2005: Formal Specification and Development in Z and B, 4th International Conference of B and Z Users Proceedings, pp.454-471, 2005.
DOI : 10.1007/11415787_26

J. Bowen and S. Reeves, Formal refinement of informal GUI design artefacts, Australian Software Engineering Conference (ASWEC'06), pp.221-230, 2006.
DOI : 10.1109/ASWEC.2006.28

&. Bowen, J. Reeves, S. Bowen, and . Reeves, Formal Models for Informal GUI Designs, Electronic Notes in Theoretical Computer Science, vol.183, pp.57-72, 2007.
DOI : 10.1016/j.entcs.2007.01.061

&. Bowen, J. Reeves, S. Bowen, and . Reeves, Using Formal Models to Design User Interfaces: A Case Study, Proceedings of the 21st British HCI Group Annual Conference on HCI 2007: HCI...but not as we know it, pp.3-7, 2007.

&. Bowen, J. Reeves, S. Bowen, and . Reeves, Formal models for user interface design artefacts, Innovations in Systems and Software Engineering, vol.31, issue.14, pp.125-141, 2008.
DOI : 10.1007/s11334-008-0049-0

&. Bowen, J. Reeves, S. Bowen, and . Reeves, Refinement for User Interface Designs, Electronic Notes in Theoretical Computer Science, vol.208, pp.5-22, 2008.
DOI : 10.1016/j.entcs.2008.03.104

J. Bowen and S. Reeves, UI-driven test-first development of interactive systems, Proceedings of the 3rd ACM SIGCHI symposium on Engineering interactive computing systems, EICS '11, pp.165-174, 2011.
DOI : 10.1145/1996461.1996515

J. Bowen and S. Reeves, Modelling user manuals of modal medical devices and learning from the experience, Proceedings of the 4th ACM SIGCHI symposium on Engineering interactive computing systems, EICS '12, pp.121-130, 2012.
DOI : 10.1145/2305484.2305505

&. Bowen, J. Reeves, S. Bowen, and . Reeves, Modelling safety properties of interactive medical systems, Proceedings of the 5th ACM SIGCHI symposium on Engineering interactive computing systems, EICS '13, pp.91-100, 2013.
DOI : 10.1145/2494603.2480314

&. Bowen, J. Reeves, S. Bowen, and . Reeves, UI-design driven model-based testing, Innovations in Systems and Software Engineering, vol.22, issue.11, pp.201-215, 2013.
DOI : 10.1007/s11334-013-0199-6

]. Bowen, Creating models of interactive systems with the support of lightweight reverse-engineering tools, Proceedings of the 7th ACM SIGCHI Symposium on Engineering Interactive Computing Systems, EICS '15, pp.110-119, 2015.
DOI : 10.1145/2774225.2774840

. Bumbulis, Combining Formal Techniques and Prototyping in User Interface Construction and Verification, 2nd Eurographics Workshop on Design, Specification, Verification of Interactive Systems (DSV-IS'95). Springer-Verlag Lecture Notes in Computer Science, pp.7-9, 1995.
DOI : 10.1007/978-3-7091-9437-9_11

. Bumbulis, A framework for machine-assisted user interface verification, Proceedings of the 4th International Conference on Algebraic Methodology and Software Technology, AMAST '95, pp.461-474, 1995.
DOI : 10.1007/3-540-60043-4_71

. Bumbulis, Validating Properties of Component-based Graphical User Interfaces, Design, Specification and Verification of Interactive Systems'96, Proceedings of the Third International Eurographics Workshop, pp.347-365, 1996.
DOI : 10.1007/978-3-7091-7491-3_18

&. Butler, W. Finelli-ricky, . Butler, B. George, and . Finelli, The Infeasibility of Quantifying the Reliability of Life-critical Real-time Software. Software Engineering, IEEE Transactions on, vol.19, issue.1, pp.3-12, 1993.

. Calvary, A Unifying Reference Framework for multi-target user interfaces, Interacting with Computers, vol.15, issue.3, pp.289-308, 2003.
DOI : 10.1016/S0953-5438(03)00010-9

. Calvary, Envisioning Advanced User Interfaces for E-Government Applications: A Case Study, Practical Studies in E-Government, pp.205-228
DOI : 10.1007/978-1-4419-7533-1_12
URL : https://hal.archives-ouvertes.fr/hal-00758011

&. Campos, C. Harrison-josé, . Campos, D. Michael, and . Harrison, Formally Verifying Interactive Systems: A Review, 1997.
DOI : 10.1007/978-3-7091-6878-3_8

&. Campos, C. Harrison-josé, . Campos, D. Michael, and . Harrison, The role of verification in interactive systems design, 1998.
DOI : 10.1007/978-3-7091-3693-5_11

&. Campos, . Harrison, C. José, . Campos, D. Michael et al., Model Checking Interactor Specifications, Automated Software Engineering, vol.8, issue.3/4, pp.275-310, 2001.
DOI : 10.1023/A:1011265604021

&. Campos, ]. Harrison, M. D. Campos, and . Harrison, Considering Context and Users in Interactive Systems Analysis, Engineering Interactive Systems -EIS 2007 Joint Working Conferences, EHCI 2007, pp.193-209, 2007.
DOI : 10.1145/1005361.1005364

&. Campos, ]. Harrison, . Campos, D. Michael, and . Harrison, Systematic Analysis of Control Panel Interfaces Using Formal Tools, Interactive Systems. Design, Specification, and Verification, pp.72-85, 2008.
DOI : 10.1007/978-3-540-70569-7_6

C. José, M. D. Campos, and . Harrison, Interaction Engineering Using the IVY Tool, Proceedings of the 1st ACM SIGCHI Symposium on Engineering Interactive Computing Systems, EICS '09, pp.35-44, 2009.

&. Campos and . Harrison, José Creissac Campos et Michael D. Harrison. Modelling and Analysing the Interactive Behaviour of an Infusion Pump, ECEASST, vol.45, 2011.

. Campos, Analysing interactive devices based on information resource constraints, International Journal of Human-Computer Studies, vol.72, issue.3, pp.284-297, 2014.
DOI : 10.1016/j.ijhcs.2013.10.005

. Carl and . Petri, Kommunikation mit Automaten, Institut für Instrumentelle Mathematik, 1962.

M. John and . Carroll, Human computer interaction-brief intro. The Interaction Design Foundation, 2013.

. Cauchi, Safer "5-key" Number Entry User Interfaces Using Differential Formal Analysis, Proceedings of the 26th Annual BCS Interaction Specialist Group Conference on People and Computers, BCS-HCI '12, pp.29-38

. Cauchi, Safer "5-key" Number Entry User Interfaces Using Differential Formal Analysis, BCS-HCI '12 Proceedings of the 26th Annual BCS Interaction Specialist Group Conference on People and Computers, BCS-HCI 2012, pp.12-14, 2012.

. Cauchi, Triangulating empirical and analytic techniques for improving number entry user interfaces, Proceedings of the 2014 ACM SIGCHI symposium on Engineering interactive computing systems, EICS '14, pp.243-252, 2014.
DOI : 10.1145/2607023.2607025

. Chériaux, François Chériaux, Dominique Galara et Marion Viel Interfaces for Nuclear Power Plant Overview, 8th International Topical Meeting on Nuclear Plant Instrumentation, Control, and Human-Machine Interface Technologies 2012 (NPIC & HMIT 2012): Enabling the Future of Nuclear Energy, NPIC & HMIT 2012, pp.1002-1012, 2012.

V. Chinnapongse, I. Lee, S. Wang, L. Paul, and . Jones, Model-Based Testing of GUI-Driven Applications, Sunggu Lee et Priya Narasimhan, pp.203-214, 2009.
DOI : 10.1007/978-3-642-10265-3_19

. Clarke, Automatic verification of finite state concurrent system using temporal logic specifications, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '83, pp.117-126, 1983.
DOI : 10.1145/567067.567080

. Cofer, Software model checking for avionics systems, 2008 IEEE/AIAA 27th Digital Avionics Systems Conference, p.5, 2008.
DOI : 10.1109/DASC.2008.4702862

. Cofer, Compositional Verification of Architectural Models, Proceedings of the 4th International Conference on NASA Formal Methods, NFM'12, pp.126-140, 2012.
DOI : 10.1007/978-3-642-28891-3_13

. Combéfis, A formal framework for design and analysis of human-machine interaction, 2011 IEEE International Conference on Systems, Man, and Cybernetics, pp.1801-1808, 2011.
DOI : 10.1109/ICSMC.2011.6083933

. Combéfis, Learning system abstractions for human operators, Proceedings of the International Workshop on Machine Learning Technologies in Software Engineering, MALETS '11, pp.3-10, 2011.
DOI : 10.1145/2070821.2070822

. Cortier, Alexandre Cortier, Bruno d'Ausbourg et Yamine Aït-Ameur. Formal Validation of Java/Swing User Interfaces with the Event B Method, Human-Computer Interaction. Interaction Design and Usability, pp.1062-1071, 2007.

. Coutaz, Software Architecture Adaptivity for Multisurface Interaction and Plasticity, Proc. of IFIP Workshop on Software Architecture Requirements for CSCW?CSCW'2000 Workshop, 2000.

. Coutaz, Joëlle Coutaz, Lionel Balme, Gaëlle Calvary, Alexandre Demeure et Jean- Sebastien Sottet. An MDE-SOA Approach to Support Plastic User Interafces in Ambient Spaces, Proc. HCI International, pp.152-171, 2007.

. Crow, Models of Mechanised Methods that Integrate Human Factors into Automation Design, International Conference on Human-Computer Interaction in Aeronautics: HCI-Aero, 2000.

. Ausbourg, Deriving a Formal Model of an Interactive System from its UIL Description in order to Verify and Test its Behaviour, Design, Specification and Verification of Interactive Systems'96, Proceedings of the Third International Eurographics Workshop, pp.105-122, 1996.

. Ausbourg, Helping the Automated Validation Process of User Interfaces Systems, Proceedings of the 20th international conference on Software engineering, ICSE '98, pp.219-228, 1998.

&. Degani and . Abbott, Asaf Degani et Michael Heymann Pilot-autopilot Interaction: A Formal Perspective, pp.157-168, 2000.

&. Degani and . Heymann, Formal Verification of Human-Automation Interaction, Human Factors: The Journal of the Human Factors and Ergonomics Society, vol.44, issue.1, pp.28-43, 2002.
DOI : 10.1518/0018720024494838

&. Degani and . Heymann, Asaf Degani et Michael Heymann Toward Automatic Generation of User Interfaces: Abstraction of Internal States and Transitions, Analysis, Design, and Evaluation of Human-Machine Systems, pp.483-489, 2007.

. Degani, Modes in Automated Cockpits: Problems, Data Analysis and a Modelling Framework, ISRAEL ANNUAL CON- FERENCE ON AEROSPACE SCIENCES, pp.258-266, 1996.

. Degani, Some Formal Aspects of Human-automation Interaction, NASA Technical Memorandum, vol.209600, 2000.

. Degani, Asaf Degani, Michael Heymann et Michael Shafto. Modeling and Formal Analysis of Human?machine Interaction. The Oxford Handbook of Cognitive Engineering, p.433, 2013.

. Demeure, Towards Run Time Plasticity Control based on a Semantic Network, Fifth International Workshop on Task Models and Diagrams for UI design (TAMODIA'06), pp.324-338, 2006.

. Demeure, COMET(s), A Software Architecture Style and an Interactors Toolkit for Plastic User Interfaces, Design, Specification, and Verification 15th International Workshop, DSV-IS 2008, pp.225-237, 2008.
DOI : 10.1007/978-3-540-70569-7_21

. Dix, Interaction models and the principled design of interactive systems, ESEC '87, 1st European Software Engineering Conference Proceedings, pp.118-126, 1987.
DOI : 10.1007/BFb0022105

A. J. Dix, Abstract, Generic Models of Interactive Systems, People and Computers IV, pp.5-9, 1988.

J. Alan and . Dix, Formal Methods: An Introduction to and Overview of the Use of Formal Methods within HCI, Chapter, vol.2, pp.9-43, 1995.

. Doherty, Representational Reasoning and Verification, Formal Aspects of Computing, vol.12, issue.4, pp.260-277, 1998.
DOI : 10.1007/PL00003934

&. Duke, J. Harrison-david, M. D. Duke, and . Harrison, Abstract Interaction Objects, Computer Graphics Forum, pp.25-36, 1993.
DOI : 10.1111/1467-8659.1230025

&. Duke, . Harrison, . Duke, and . Harrison, Event model of human-system interaction, Software Engineering Journal, vol.10, issue.1, pp.3-12, 1995.
DOI : 10.1049/sej.1995.0002

. Duke, Systematic development of the human interface, Proceedings 1995 Asia Pacific Software Engineering Conference, p.313, 1995.
DOI : 10.1109/APSEC.1995.496980

. Duke, A Case Study in the Specification and Analysis of Design Alternatives for a User Interface, Formal Aspects of Computing, vol.11, issue.2, pp.107-131, 1999.
DOI : 10.1007/s001650050044

C. Matthew, . Elder, and . Knight, Specifying User Interfaces for Safetycritical Medical Systems, Proc. of the 2nd Annual International Symposium on Medical Robotics and Computer Assisted Surgery, pp.148-155, 1995.

&. Faconti, P. Paternó-giorgio, F. Faconti, and . Paternó, An Approach to the Formal Specification of the Components of an Interaction, 1990.

. Fernandez, CADP a protocol validation and verification toolbox, Proceedings of the 8th Conference on Computer-Aided Verification, pp.437-440, 1996.
DOI : 10.1007/3-540-61474-5_97

. Fields, Modelling Interactive Systems and Providing Task Relevant Information, Interactive Systems: Design, Specification, and Verification, pp.253-266, 1995.
DOI : 10.1007/978-3-642-87115-3_15

. Fields, Applying formal methods for human error tolerant design, Software Engineering and Human-Computer Interaction, pp.185-195, 1995.
DOI : 10.1007/BFb0035815

. Fields, A task centered approach to analysing human error tolerance requirements, Proceedings of 1995 IEEE International Symposium on Requirements Engineering (RE'95), pp.18-26, 1995.
DOI : 10.1109/ISRE.1995.512542

&. Foley, ]. J. Wallace-1974, V. L. Foley, and . Wallace, The art of natural graphic man-machine conversation, ACM SIGGRAPH Computer Graphics, vol.8, issue.3, pp.87-87, 1974.
DOI : 10.1145/988026.988037

. Ganneau, Learning Key Contexts of Use in the Wild for Driving Plastic User Interfaces Engineering, Engineering Interactive Systems 2008 (2nd Conference on Human-Centred Software Engineering (HCSE 2008) and 7th International workshop on TAsk MOdels and DIAgrams, 2008.
DOI : 10.1007/978-3-540-85992-5_26

&. Garavel, . Graf, S. Garavel, and . Graf, Formal Methods for Safe and Secure Computer Systems. Federal Office for Information Security, 2013.

H. Garavel and F. Lang, SVL: A Scripting Language for Compositional Verification, Proceedings of the 21st IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems FORTE'2001, pp.377-392, 2001.
DOI : 10.1007/0-306-47003-9_24
URL : https://hal.archives-ouvertes.fr/inria-00072396

. Garavel, An Overview of CADP, Frédéric Lang et Radu Mateescu, pp.13-24, 2001.
URL : https://hal.archives-ouvertes.fr/inria-00069920

. Garavel, CADP??2006: A Toolbox for the Construction and Analysis of Distributed Processes, Proceedings of the 19th International Conference on Computer Aided Verification CAV, pp.158-163, 2007.
DOI : 10.1007/978-3-540-73368-3_18
URL : https://hal.archives-ouvertes.fr/inria-00189021

. Garavel, CADP 2011: a toolbox for the construction and analysis of distributed processes, International Journal on Software Tools for Technology Transfer, vol.1, issue.1/2, pp.89-107, 2013.
DOI : 10.1007/s10009-012-0244-z
URL : https://hal.archives-ouvertes.fr/hal-00715056

H. Garavel, F. Lang, and R. Mateescu, Compositional verification of asynchronous concurrent systems using CADP, Acta Informatica, vol.56, issue.1/2, pp.1-56, 2015.
DOI : 10.1007/s00236-015-0226-1
URL : https://hal.archives-ouvertes.fr/hal-01247507

A. Gimblett and H. W. Thimbleby, User interface model discovery, Proceedings of the 2nd ACM SIGCHI symposium on Engineering interactive computing systems, EICS '10, pp.145-154, 2010.
DOI : 10.1145/1822018.1822041

&. Gimblett, A. Thimbleby, H. Gimblett, and . Thimbleby, Applying theorem discovery to automatically find and check usability heuristics, Proceedings of the 5th ACM SIGCHI symposium on Engineering interactive computing systems, EICS '13, pp.101-106, 2013.
DOI : 10.1145/2494603.2480320

. Godefroid, Transferring Formal Methods Technology to Industry, wift, p.128, 1998.

. Hallinger, Systems Thinking/Systems Changing & A Computer Simulation for Learning How to Make School Ssmarter Advances in Research and Theories of School Management and Educational Policy, pp.15-24, 2000.

. Hamilton, Experiences in applying formal methods to the analysis of software and system requirements, Proceedings of 1995 IEEE Workshop on Industrial-Strength Formal Specification Techniques, pp.30-43, 1995.
DOI : 10.1109/WIFT.1995.515477

. Hardin, Development of Security Software: A High Assurance Methodology, Formal Methods and Software Engineering, 11th International Conference on Formal Engineering Methods. Proceedings, pp.266-285, 2009.
DOI : 10.1007/978-3-642-10373-5_14

&. Harrison, D. Michael, . Harrison, J. David, and . Duke, A review of formalisms for describing interactive behaviour, Software Engineering and Human-Computer Interaction, pp.49-75, 1995.
DOI : 10.1007/BFb0035807

. Harrison, The User Context and Formal Specification in Interactive System Design, Proceedings of the 1996 BCS-FACS conference on Formal Aspects of the Human Computer Interface, pp.5-5, 1996.

. Harrison, Automated Theorem Proving for the Systematic Analysis of an Infusion Pump, 2013.

. Harrison, Reusing models and properties in the analysis of similar interactive devices, Innovations in Systems and Software Engineering, vol.36, issue.51, pp.95-111, 2015.
DOI : 10.1007/s11334-013-0201-3

&. Heymann and . Degani, Michael Heymann et Asaf Degani On the Construction of Humanautomation Interfaces by Formal Abstraction, Abstraction, Reformulation, and Approximation, pp.99-115, 2002.

&. Heymann and . Degani, Formal Analysis and Automatic Generation of User Interfaces: Approach, Methodology, and an Algorithm, Human Factors, vol.11, issue.2, pp.311-330, 2007.
DOI : 10.1518/001872007X312522

&. Hix, D. Hix, and H. R. Hartson, Developing User Interfaces: Ensuring Usability Through Product &Amp; Process, 1993.

. Hjort, Model-Based GUI Testing Using Uppaal?? at Novo Nordisk, FM 2009: Formal Methods, pp.814-818, 2009.
DOI : 10.1007/978-3-642-05089-3_53

&. Huang, . Lu, L. Huang, and . Lu, Apply ant colony to event-flow model for graphical user interface test case generation, IET Software, vol.6, issue.1, pp.50-60, 2012.
DOI : 10.1049/iet-sen.2011.0012

&. Imaz, M. Benyon, D. Imaz, and . Benyon, Designing with Blends: Conceptual Foundations of Human-computer Interaction and Software Engineering Methods, 2007.

. Jacky, Modelbased Software Testing and Analysis with C#, 2007.

. Jambon, Interactive System Safety and Usability Enforced with the Development Process, Engineering for Human- Computer Interaction, 8th IFIP International Conference, pp.39-56, 2001.
DOI : 10.1007/3-540-45348-2_8

C. John, . Knight, S. Susan, and . Brilliant, Preliminary Evaluation of a Formal Approach to User Interface Specification. In ZUM'97: The Z Formal Specification Notation, pp.329-346, 1997.

&. Knight, C. Kienzle-]-john, D. M. Knight, and . Kienzle, Preliminary Experience Using Z to Specify a Safety-Critical System, Proceedings, pp.14-15, 1992.
DOI : 10.1007/978-1-4471-3556-2_8

. Knight, Tool Support for Production Use of Formal Techniques, FM'99 -Formal Methods, World Congress on Formal Methods in the Development of Computing Systems Proceedings, Volume II, p.1854, 1999.

C. John and . Knight, Challenges in the Utilization of Formal Methods, Formal Techniques in Real-Time and Fault-Tolerant Systems, pp.1-17, 1998.

G. Nancy and . Leveson, Safeware: System Safety and Computers, 1995.

. Li, Exploring the Effect of Pre-operational Priming Intervention on Number Entry Errors, Proceedings of the 33rd Annual ACM Conference on Human Factors in Computing Systems, CHI '15, pp.1335-1344, 2015.
DOI : 10.1145/2702123.2702477

&. Loer, K. Harrison, M. D. Loer, and . Harrison, Formal Interactive Systems Analysis and Usability Inspection Methods: Two Incompatible Worlds?, DSV-IS, pp.169-190, 2000.
DOI : 10.1007/3-540-44675-3_11

K. Loer and M. Harrison, Towards usable and relevant model checking techniques for the analysis of dependable interactive systems, Proceedings 17th IEEE International Conference on Automated Software Engineering,, pp.223-226, 2002.
DOI : 10.1109/ASE.2002.1115016

&. Loer, K. Harrison, . Loer, D. Michael, and . Harrison, An integrated framework for the analysis of dependable interactive systems (IFADIS): Its tool support and evaluation, Automated Software Engineering, vol.12, issue.4, pp.469-496, 2006.
DOI : 10.1007/s10515-006-7999-y

&. Lu, L. Huang, Y. Lu, and . Huang, Automated GUI Test Case Generation, 2012 International Conference on Computer Science and Service System, pp.582-585, 2012.
DOI : 10.1109/CSSS.2012.151

R. Robyn and . Lutz, Software Engineering for Safety: a Roadmap, Proceedings of the Conference on The Future of Software Engineering, pp.213-226, 2000.

&. Madani and . Parissis, Automatically testing interactive applications using extended task trees, The Journal of Logic and Algebraic Programming, vol.78, issue.6, pp.454-471, 2009.
DOI : 10.1016/j.jlap.2009.01.005
URL : https://hal.archives-ouvertes.fr/hal-00380724

. Mariani, AutoBlackTest, Proceeding of the 33rd international conference on Software engineering, ICSE '11, pp.1013-1015, 2011.
DOI : 10.1145/1985793.1985979

. Markopoulos, Dialogue Modelling in the Framework of an Interactor Model, Pre-conference Proceedings. Design Specification and Verification of Interactive Systems, 1996.

. Markopoulos, Formal architectural abstractions for interactive software, International Journal of Human-Computer Studies, vol.49, issue.5, pp.675-715, 1998.
DOI : 10.1006/ijhc.1998.0223

. Martinie, A multi-formalism approach for model-based dynamic distribution of user interfaces of critical interactive systems, International Journal of Human-Computer Studies, vol.72, issue.1, pp.77-99, 2014.
DOI : 10.1016/j.ijhcs.2013.08.013
URL : https://hal.archives-ouvertes.fr/hal-01130579

. Masci, On Formalising Interactive Number Entry on Infusion Pumps, Electronic Communications of the EASST, vol.45, 2011.

. Masci, Verification of interactive software for medical devices, Proceedings of the 5th ACM SIGCHI symposium on Engineering interactive computing systems, EICS '13, pp.81-90, 2013.
DOI : 10.1145/2494603.2480302

. Masci, Model-Based Development of the Generic PCA Infusion Pump User Interface Prototype in PVS, Proceedings of the 32Nd International Conference on Computer Safety, Reliability, and Security, pp.228-240, 2013.
DOI : 10.1007/978-3-642-40793-2_21

. Masci, Formal Verification of Medical Device User Interfaces Using PVS, Proceedings of the 17th International Conference on Fundamental Approaches to Software Engineering, pp.200-214, 2014.
DOI : 10.1007/978-3-642-54804-8_14

. Masci, Combining PVSio with Stateflow, NASA Formal Methods -6th International Symposium, NFM 2014. Proceedings, pp.209-214, 2014.
DOI : 10.1007/978-3-319-06200-6_16

. Masci, The benefits of formalising design guidelines: a case study on the predictability of drug infusion pumps, Innovations in Systems and Software Engineering, vol.54, issue.3, pp.73-93, 2015.
DOI : 10.1007/s11334-013-0200-4

&. Mateescu and . Oudot, Bisimulator 2.0: An On-the-Fly Equivalence Checker based on Boolean Equation Systems, 2008 6th ACM/IEEE International Conference on Formal Methods and Models for Co-Design, pp.73-74, 2008.
DOI : 10.1109/MEMCOD.2008.4547690
URL : https://hal.archives-ouvertes.fr/inria-00357770

P. Steven, . Miller, W. Michael, . Whalen, D. Darren et al., Software Model Checking Takes off, Communications of the ACM, vol.53, issue.2, pp.58-64, 2010.

P. Steven and . Miller, Bridging the Gap Between Model-based Development and Model Checking, Tools and Algorithms for the Construction and Analysis of Systems, pp.443-453, 2009.

&. Mital and . Pennathur, Advanced technologies and humans in manufacturing workplaces: an interdependent relationship, International Journal of Industrial Ergonomics, vol.33, issue.4, pp.295-313, 2004.
DOI : 10.1016/j.ergon.2003.10.002

. Miñón, An Approach to the Integration of Accessibility Requirements into a User Interface Development Method, Special issue on Software Support for User Interface Description Languages, pp.58-73, 2011.

. Mori, CTTE: support for developing and analyzing task models for interactive system design, IEEE Transactions on Software Engineering, vol.28, issue.8, pp.797-813, 2002.
DOI : 10.1109/TSE.2002.1027801

. Murugesan, Sanjai Rayadurgam et Mats Per Erik Heimdahl Compositional Verification of a Medical Device System, Proceedings of the 2013 ACM SIGAda annual conference on High integrity language technology, HILT 2013, pp.51-64, 2013.

. Navarre, A Tool Suite for Integrating Task and System Models through Scenarios, Proceedings of the 8th International Workshop on Interactive Systems: Design, Specification, and Verification-Revised Papers, DSV-IS '01, pp.88-113, 2001.
DOI : 10.1007/3-540-45522-1_6

. Navarre, A Formal Description of Multimodal Interaction Techniques for Immersive Virtual Reality Applications, Proceedings of the 2005 IFIP TC13 International Conference on Human-Computer Interaction, INTERACT'05, pp.170-183, 2005.
DOI : 10.1006/ijhc.2001.0474

. Navarre, A Formal Approach for User Interaction Reconfiguration of Safety Critical Interactive Systems, Computer Safety, Reliability, and Security, pp.373-386, 2008.
DOI : 10.1007/978-3-540-87698-4_31

. Navarre, ICOs, ACM Transactions on Computer-Human Interaction, vol.16, issue.4, 2009.
DOI : 10.1145/1614390.1614393

. Nguyen, Model-based testing of multiple GUI variants using the GUI test generator, Proceedings of the 5th Workshop on Automation of Software Test, AST '10, pp.24-30, 2010.
DOI : 10.1145/1808266.1808270

. Nguyen, GUITAR: an innovative tool for automated testing of GUI-driven software, Automated Software Engineering, vol.37, issue.4, pp.65-105, 2014.
DOI : 10.1007/s10515-013-0128-9

&. Nielsen, J. Landauer, . Nielsen, K. Thomas, and . Landauer, A mathematical model of the finding of usability problems, Proceedings of the SIGCHI conference on Human factors in computing systems , CHI '93, pp.206-213, 1993.
DOI : 10.1145/169059.169166

. Niwa, The Design of Human???Machine Interface for Accident Support in Nuclear Power Plants, Cognition, Technology & Work, vol.3, issue.3, pp.161-176, 2001.
DOI : 10.1007/PL00011531

. Oladimeji, Number Entry Interfaces and Their Effects on Error Detection, Human-Computer Interaction -INTERACT 2011 -13th IFIP TC 13 International Conference Proceedings, Part IV, pp.178-185, 2011.
DOI : 10.1007/978-3-642-23768-3_15

. Oladimeji, A Performance Review of Number Entry Interfaces, Human-Computer Interaction -INTERACT 2013 -14th IFIP TC 13 International Conference Proceedings, Part I, pp.365-382, 2013.
DOI : 10.1007/978-3-642-40483-2_26
URL : https://hal.archives-ouvertes.fr/hal-01497448

. Oliveira, Formal Verification of UI Using the Power of a Recent Tool Suite, Proceedings of the 2014 ACM SIGCHI Symposium on Engineering Interactive Computing Systems, pp.235-240, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01110183

. Oliveira, Equivalence checking for comparing user interfaces, Proceedings of the 7th ACM SIGCHI Symposium on Engineering Interactive Computing Systems, EICS '15, pp.266-275, 2015.
DOI : 10.1145/2774225.2774844
URL : https://hal.archives-ouvertes.fr/hal-01247496

. Oliveira, Plasticity of user interfaces, Proceedings of the 7th ACM SIGCHI Symposium on Engineering Interactive Computing Systems, EICS '15, pp.260-265, 2015.
DOI : 10.1145/2774225.2775078
URL : https://hal.archives-ouvertes.fr/hal-01247489

. Oliveira, Abstract, De Gruyter publication Journal of Interactive Media, pp.192-204, 2015.
DOI : 10.1515/icom-2015-0036
URL : https://hal.archives-ouvertes.fr/hal-00973399

R. Dan and . Olsen-jr, Evaluating User Interface Systems Research, Proceedings of the 20th annual ACM symposium on User interface software and technology, pp.251-258, 2007.

&. Palanque, A. Bastide-philippe, R. Palanque, and . Bastide, Petri Net Based Design of User-Driven Interfaces Using the Interactive Cooperative Objects Formalism, Interactive systems: Design, specification, and verification, pp.383-400, 1995.
DOI : 10.1007/978-3-642-87115-3_23

. Palanque, Validating interactive system design through the verification of formal task and system models, Proceedings of the IFIP TC2/WG2.7 Working Conference on Engineering for Human-Computer Interaction, pp.189-212, 1996.
DOI : 10.1007/978-0-387-34907-7_11

. Palanque, Formal Specification as a Tool for Objective Assessment of Safety-Critical Interactive Systems, Proceedings of the IFIP TC13 Interantional Conference on Human-Computer Interaction, INTERACT '97, pp.323-330, 1997.
DOI : 10.1007/978-0-387-35175-9_53

. Palanque, Embedding Ergonomic Rules As Generic Requirements in a Formal Development Process of Interactive Software, Human-Computer Interaction INTERACT '99: IFIP TC13 International Conference on Human-Computer Interaction, pp.408-416, 1999.

&. Paternò, F. Faconti, G. Paternò, and . Faconti, On the Use of LOTOS to Describe Graphical Interaction. People and computers, pp.155-155, 1992.

&. Paternó and . Mezzanotte, Fabio Paternó et Menica Mezzanotte Analysing MATIS by Interactors and ACTL. The AMODEUS Project?ESPRIT BRA 7040, Report SM, vol.36, 1994.

&. Paternò, F. Paternò, and M. Mezzanotte, Formal verification of undesired behaviours in the CERD case study, Proceedings of the IFIP TC2/WG2.7 Working Conference on Engineering for Human-Computer Interaction, pp.213-226, 1996.
DOI : 10.1007/978-0-387-34907-7_12

&. Paternò, F. Santoro, C. Paternò, and . Santoro, Integrating Model Checking and HCI Tools to Help Designers Verify User Interface Properties, Proceedings of the 7th International Conference on Design, Specification, and Verification of Interactive Systems, DSV-IS'00, pp.135-150, 2001.
DOI : 10.1007/3-540-44675-3_9

F. Paternò and C. Santoro, Support for Reasoning about Interactive Systems through Human-Computer Interaction Designers' Representations, The Computer Journal, vol.46, issue.4, pp.340-357, 2003.
DOI : 10.1093/comjnl/46.4.340

. Paternò, ConcurTaskTrees: A Diagrammatic Notation for Specifying Task Models, Proceedings of the IFIP TC13 Interantional Conference on Human-Computer Interaction, INTERACT '97, pp.362-369, 1997.
DOI : 10.1007/978-0-387-35175-9_58

]. F. Paternó, A Theory of User-interaction Objects, Journal of Visual Languages & Computing, vol.5, issue.3, pp.227-249, 1994.
DOI : 10.1006/jvlc.1994.1012

]. F. Paternó, Formal reasoning about dialogue properties with automatic support, Interacting with Computers, vol.9, issue.2, pp.173-196, 1997.
DOI : 10.1016/S0953-5438(97)00015-5

. Preece, Human-computer Interaction, 1994.

J. Queille and J. Sifakis, Specification and verification of concurrent systems in CESAR, Proceedings of the 5th Colloquium on International Symposium on Programming, pp.337-351, 1982.
DOI : 10.1007/3-540-11494-7_22

J. Queille and J. Sifakis, Fairness and related properties in transition systems ? a temporal logic to deal with fairness, Acta Informatica, vol.19, issue.3, pp.195-220, 1983.
DOI : 10.1007/BF00265555

&. Rushby, M. Von-henke-john, . Rushby, W. Friedrich, and . Von-henke, Formal verification of algorithms for critical systems, IEEE Transactions on Software Engineering, vol.19, issue.1, pp.13-23, 1993.
DOI : 10.1109/32.210304

. Rushby, An automated method to detect potential mode confusions, Gateway to the New Millennium. 18th Digital Avionics Systems Conference. Proceedings (Cat. No.99CH37033), p.4, 1999.
DOI : 10.1109/DASC.1999.863725

M. John and . Rushby, Analyzing Cockpit Interfaces Using Formal Methods, Electr. Notes Theor. Comput. Sci, vol.43, pp.1-14, 2001.

. Serna, How assessing plasticity design choices can improve UI quality, Proceedings of the 2nd ACM SIGCHI symposium on Engineering interactive computing systems, EICS '10, pp.29-34, 2010.
DOI : 10.1145/1822018.1822024
URL : https://hal.archives-ouvertes.fr/hal-00953316

. Shiffman, Smadar Shiffman, Asaf Degani et Michael Heymann Ui Verify ? A Web-based Tool for Verification and Automatic Generation of User Interfaces. interfaces, p.4, 2004.

. Silva, Combining Formal Methods and Functional Strategies Regarding the Reverse Engineering of Interactive Applications, Proceedings of the 13th International Conference on Interactive Systems: Design, Specification, and Verification, DSVIS'06, pp.137-150, 2007.
DOI : 10.1007/978-3-540-69554-7_11

. Sottet, Mapping Model: A First Step to Ensure Usability for Sustaining User Interface Plasticity, 2006.

. Sottet, A language perspective on the development of plastic multimodal user interfaces, Journal on Multimodal User Interfaces, vol.12, issue.no. 2, 2007.
DOI : 10.1007/BF02910054

. Sousa, Formal Verification of Safety-critical User Interfaces: A Space System Case Study, Formal Verification and Modeling in Human Machine Systems: Papers from the AAAI Spring Symposium, pp.62-67, 2014.

]. J. Spivey, The Z Notation: A Reference Manual, 1989.

. Strunk, Echo, Proceedings of the 10th international workshop on Formal methods for industrial critical systems , FMICS '05, pp.44-53, 2005.
DOI : 10.1145/1081180.1081187

&. Thevenin and . Coutaz, David Thevenin et Joëlle Coutaz Plasticity of User Interfaces: Framework and Research Agenda, Proceedings of INTERACT, pp.110-117, 1999.

&. Thimbleby, J. Thimbleby, and . Gow, Applying Graph Theory to Interaction Design, Engineering Interactive Systems, pp.501-519, 2008.
DOI : 10.1038/30918

]. Thimbleby, Interaction Walkthrough: Evaluation of Safety Critical Interactive Systems, Interactive Systems. Design, Specification, and Verification, pp.52-66, 2007.
DOI : 10.1007/978-3-540-69554-7_5

]. Thimbleby, User-Centered Methods Are Insufficient for Safety Critical Systems, 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, USAB'07, pp.1-20, 2007.
DOI : 10.1007/978-3-540-76805-0_1

. Tsai, Automatic Test Case Generation for GUI Navigation, Quality Week, 2000.

. Tu, "The Effects of Number-related Factors on Entry Performance", 2014.
DOI : 10.14236/ewic/hci2014.31

S. Clark and . Turner, An Investigation of the Therac-25, Accidents. COMPUTER, vol.1893, issue.9I62, pp.700-001830300, 1993.

&. Van-glabbeek, . Weijland, J. Rob, W. Van-glabbeek, and . Peter-weijland, Branching time and abstraction in bisimulation semantics, Journal of the ACM, vol.43, issue.3, pp.555-600, 1996.
DOI : 10.1145/233551.233556

. Vanderdonckt, Multimodality for Plastic User Interfaces: Models, Methods, and Principles, chapitres d'ouvrages 4, Lecture Notes in Electrical Engineering, pp.61-84, 2007.

&. Wang, G. Wang, and . Abowd, A Tabular Interface for Automated Verification of Event-based Dialogs. Rapport technique, DTIC Document, 1994.

. Whalen, Integration of Formal Analysis into a Model-Based Software Development Process, Formal Methods for Industrial Critical Systems, pp.68-84, 2008.
DOI : 10.1007/978-3-540-79707-4_7

C. Xiang-yin-et-john and . Knight, Formal Verification of Large Software Systems, Second NASA Formal Methods Symposium -NFM 2010 Proceedings, pp.192-201, 2010.

. Yin, Formal Verification by Reverse Synthesis, Computer Safety, Reliability, and Security, 27th International Conference Proceedings, pp.305-319, 2008.
DOI : 10.1007/978-3-540-87698-4_26

J. Knight and W. Weimer, Exploiting Refactoring in Formal Verification, Dependable Systems & Networks, 2009. DSN'09. IEEE/IFIP International Conference on, pp.53-62, 2009.

C. John, W. Knight, and . Weimer, Exploiting Refactoring in Formal Verification, Proceedings of the 2009 IEEE/IFIP International Conference on Dependable Systems and Networks, pp.53-62, 2009.