, Ed 143 -minimum operational performance standards for traffic alert and collision avoidance system ii (tcas ii), 2013.

A. John and . Bargh, The Four Horsemen of Automaticity: Awareness, Efficiency, Intention, and Control in Social Cognition, vol.2, 1994.

J. , The B-book: Assigning Programs to Meanings, 1996.

A. Mga-ament, A. Cox, D. Blandford, and . Brumby, Working memory load affects device-specific but not taskspecific error rate, CogSci 2010: Proceedings of the Annual Conference of the Cognitive Science Society, pp.91-96, 2010.

H. Anderson and G. Ciobanu, Markov abstractions for probabilistic pi-calculus, Electronic Communications of the EASST, vol.22, 2009.

M. Arapinis, M. Calder, L. Denis, M. Fisher, P. Gray et al., Towards the verification of pervasive systems, Electronic Communications of the EASST, vol.22, 2009.

J. C. Baeten, A brief history of process algebra, Process Algebra, vol.335, pp.131-146, 2005.

C. Baier and J. Katoen, Principles of Model Checking (Representation and Mind Series), p.9780262026499, 2008.

R. Banach, J. Razavi, O. Debicki, N. Mareau, S. Lesecq et al., Application of formal methods in the inspex smart systems integration project, vol.5, 2018.

M. A. Barbosa, L. Soares-barbosa, and J. Campos, Towards a coordination model for interactive systems, Proceedings of the First International Workshop on Formal Methods for Interactive Systems, vol.183, pp.89-103, 2007.

M. Barnett, The spec# programming system: An overview, CASSIS 2004, Construction and Analysis of Safe, Secure and Interoperable Smart devices, vol.3362, pp.49-69, 2005.

E. J. Bass, K. M. Feigh, E. Gunter, and J. Rushby, Formal modeling and analysis for interactive hybrid systems, vol.45, p.2011

M. Beaudouin-lafon, Designing interaction, not interfaces, Proceedings of the Working Conference on Advanced Visual Interfaces, AVI '04, pp.15-22, 2004.

B. Beckert and G. Beuster, Guaranteeing consistency in text-based human-computer-interaction, Proceedings of the First International Workshop on Formal Methods for Interactive Systems, 2007.

G. Behrmann, A. David, and K. G. Larsen, A Tutorial on Uppaal, pp.200-236, 2004.

C. Bhandal, M. Bouroche, and A. Hughes, A process algebraic description of a temporal wireless network protocol, vol.45, p.2011

S. Bhattacharya and A. Basu, Some issues in modeling the performance of soft keyboards with scanning, Proceedings of the First International Workshop on Formal Methods for Interactive Systems, 2007.

S. Boldo, C. Lelay, and G. Melquiond, Formalization of Real Analysis: A Survey of Proof Assistants and Libraries, Mathematical Structures in Computer Science, vol.26, issue.7, pp.1196-1233, 2016.
URL : https://hal.archives-ouvertes.fr/hal-00806920

J. Bonnefon, D. Longin, and M. Nguyen, A logical framework for trust-related emotions. Electronic Communications of the EASST, vol.22, 2009.

J. Bowen and A. Hinze, Supporting mobile application development with model-driven emulation, vol.45, 2011.

J. Bowen and S. Reeves, Formal models for informal gui designs, Proceedings of the First International Workshop on Formal Methods for Interactive Systems, vol.183, pp.57-72, 2007.

J. Bowen and S. Reeves, Refinement for user interface designs, Proceedings of the 2nd International Workshop on Formal Methods for Interactive Systems, vol.208, pp.5-22, 2008.

J. Bowen and S. Reeves, Ui-design driven model-based testing, Electronic Communications of the EASST, vol.22, 2009.

P. Béger, V. Becquet, S. Leriche, and D. Prun, Contribution à la formalisation des propriétés graphiques des systèmes interactifs pour la validation automatique, Afadl 2019, 18èmes journées Approches Formelles dans l'Assistance au Developpement de Logiciels, 2019.

B. Bérard, Systems and Software Verification: Model-Checking Techniques and Tools, vol.3642074782, p.9783642074783, 2010.

M. Calder, P. Gray, and C. Unsworth, Tightly coupled verification of pervasive systems, Electronic Communications of the EASST, vol.22, 2009.

J. Campos and M. Harrison, Modelling and analysing the interactive behaviour of an infusion pump, vol.45, 2011.

D. Cansell, J. P. Gibson, and D. Méry, Refinement: A constructive approach to formal software design for a secure e-voting interface, Proceedings of the First International Workshop on Formal Methods for Interactive Systems, vol.183, pp.39-55, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00594892

U. Cartwright, -. Finch, and N. Lavie, The role of perceptual load in inattentional blindness, Cognition, vol.102, issue.3, pp.321-340, 2007.

A. Cerone, Closure and attention activation in human automatic behaviour: A framework for the formal analysis of interactive systems, vol.45, p.2011

A. Cerone, Towards a cognitive architecture for the formal analysis of human behaviour and learning, Software Technologies: Applications and Foundations, pp.216-232, 2018.

A. Cerone and N. Elbegbayan, Model-checking driven design of interactive systems, Proceedings of the First International Workshop on Formal Methods for Interactive Systems, vol.183, pp.3-20, 2007.

A. Cerone and Y. Zhao, Stochastic modelling and analysis of driver behaviour, ECEASST, p.69, 2013.

R. Cleaveland, T. Li, and S. Sims, The concurrency workbench of the new century, 2000.

R. David and H. Alla, Discrete, Continuous, and Hybrid Petri Nets, p.9783642106682
URL : https://hal.archives-ouvertes.fr/hal-00495611

L. De-moura, S. Owre, H. Rueß, J. Rushby, N. Shankar et al., Sal 2, Computer Aided Verification, pp.496-500, 2004.

A. Dittmar and R. Schachtschneider, Lightweight interaction modeling in evolutionary prototyping, ECEASST, p.69, 2013.

A. Dittmar, T. Hübner, and P. Forbrig, Hops: A prototypical specification tool for interactive systems, Interactive Systems. Design, Specification, and Verification, pp.58-71, 2008.

A. Dix, M. Ghazali, and D. , Modelling devices for natural interaction. Electronic Notes in Theoretical Computer Science, Proceedings of the 2nd International Workshop on Formal Methods for Interactive Systems, vol.208, pp.23-40, 2008.
URL : https://hal.archives-ouvertes.fr/hal-00534919

J. E. Raymond, K. Shapiro, and K. Arnell, Temporary suppression of visual processing in an rsvp task: An attentional blink? Journal of experimental psychology. Human perception and performance, vol.18, pp.849-60, 1992.

R. Geniet and N. Singh, Refinement based formal development of human-machine interface, Software Technologies: Applications and Foundations, pp.240-256, 2018.
URL : https://hal.archives-ouvertes.fr/hal-02353335

D. Goldson, G. Reeve, and S. Reeves, µ-chart-based specification and refinement, Proceedings of the 4th International Conference on Formal Engineering Methods: Formal Methods and Software Engineering, ICFEM '02, pp.323-334, 2002.

V. Goranko and A. Galton, Temporal logic. The Stanford Encyclopedia of Philosophy, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01054932

A. Gosain and G. Sharma, Static analysis: A survey of techniques and tools, Intelligent Computing and Applications, pp.581-591, 2015.

M. D. Harrison, C. Kray, and J. Campos, Exploring an option space to engineer a ubiquitous computing system, Proceedings of the 2nd International Workshop on Formal Methods for Interactive Systems, vol.208, pp.41-55, 2008.

M. D. Harrison, P. Masci, J. C. Campos, and P. Curzon, Automated theorem proving for the systematic analysis of an infusion pump, ECEASST, p.69, 2013.

M. D. Harrison, P. Masci, and J. Campos, Formal modelling as a component of user centred design, Software Technologies: Applications and Foundations, pp.274-289, 2018.

J. Hillston, A Compositional Approach to Performance Modelling, 1996.

C. A. Hoare, Communicating Sequential Processes, 1985.

G. Holzmann, The SPIN Model Checker: Primer and Reference Manual, p.9780321773715, 2011.

H. Huang, R. Ruk??nas, M. Ament, P. Curzon, A. Cox et al., Capturing the distinction between task and device errors in a formal model of user behaviour, vol.45, 2011.

, Information processing systems -open systems interconnection -lotos -a formal description technique based on the temporal ordering of observational behaviour, 1989.

C. W. Johnson, Using assurance cases and boolean logic driven markov processes to formalise cyber security concerns for safety-critical interaction with global navigation satellite systems, vol.45, p.2011

C. Kray, G. Kortuem, and A. Krüger, Adaptive navigation support with public displays, Proceedings of the 10th International Conference on Intelligent User Interfaces, IUI '05, pp.326-328, 2005.

S. Leriche, S. Conversy, C. Picard, D. Prun, and M. Magnaudet, Towards handling latency in interactive software, Software Technologies: Applications and Foundations, pp.233-239, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01815224

P. Masci, P. Curzon, A. Blandford, and D. Furniss, Modelling distributed cognition systems in pvs, vol.45, 2011.

P. Masci, R. Ruk??nas, P. Oladimeji, A. Cauchi, A. Gimblett et al., On formalising interactive number entry on infusion pumps, vol.45, p.2011

G. Mori, F. Paterno, and C. Santoro, Design and development of multidevice user interfaces through multiple logical descriptions, IEEE Transactions on Software Engineering, vol.30, issue.8, pp.507-520, 2004.

B. A. Myers and M. B. Rosson, Survey on user interface programming, Proceedings of the SIGCHI Conference on Human Factors in Computing Systems, CHI '92, pp.195-202

D. Navarre, P. Palanque, J. Ladry, and E. Barboni, Icos: A model-based user interface description technique dedicated to interactive systems addressing usability, reliability and scalability, ACM Trans. Comput.-Hum. Interact, vol.16, issue.4, p.56, 2009.

G. Norman, C. Palamidessi, D. Parker, and P. Wu, Model checking the probabilistic ?-calculus, Proc. 4th International Conference on Quantitative Evaluation of Systems (QEST'07), pp.169-178, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00201069

P. Oladimeji, P. Masci, P. Curzon, and H. Thimbleby, Pvsio-web: a tool for rapid prototyping device user interfaces in pvs, ECEASST, p.69, 2013.

S. Owicki and L. Lamport, Proving liveness properties of concurrent programs, ACM Trans. Program. Lang. Syst, vol.4, issue.3, pp.455-495, 1982.

P. Puschner and A. Burns, A review of worst-case execution-time analyses. Real-time Systems -RTS, vol.01, 1999.

R. Ruk??nas, P. Curzon, and A. Blandford, Detecting cognitive causes of confidentiality leaks, Proceedings of the First International Workshop on Formal Methods for Interactive Systems, vol.183, pp.21-38, 2007.

R. Ruk??nas, J. Back, P. Curzon, and A. Blandford, Formal modelling of salience and cognitive load, Proceedings of the 2nd International Workshop on Formal Methods for Interactive Systems, vol.208, pp.57-75, 2008.

R. Ruk??nas and P. Curzon, Abstract models and cognitive mismatch in formal verification, vol.45, 2011.

R. Ruk??nas, P. Masci, M. D. Harrison, and P. Curzon, Developing and verifying user interface requirements for infusion pumps: A refinement approach, ECEASST, p.69, 2013.

D. Mark, B. Ryan, and . Smyth, Applied pi calculus, Formal Models and Techniques for Analyzing Security Protocols, chapter 6, 2011.

A. Sabelfeld and A. C. Myers, Language-based information-flow security, IEEE J.Sel. A. Commun, vol.21, issue.1, pp.733-8716, 2006.

D. Sannella and M. Wirsing, Specification languages. Algebraic Foundation of Systems Specification. IFIP State-ofthe-Art Reports, vol.07, pp.243-272, 1999.

, Working Group 71. Rtca/do-178c software considerations in airborne systems and equipment certification, 2011.

, Working Group 71. Rtca/do-333 formal methods supplement to do-178c and do-278a, 2011.

N. Shankar, Pvs: Combining specification, proof checking, and model checking, Formal Methods in Computer-Aided Design, pp.257-264, 1996.

L. José, J. Silva, A. C. Creissac-campos, and . Paiva, Model-based user interface testing with spec explorer and concurtasktrees, Proceedings of the 2nd International Workshop on Formal Methods for Interactive Systems, vol.208, pp.77-93, 2008.

J. Silva, C. Fayollas, A. Hamon, P. Palanque, C. Martiinie et al., Analysis of wimp and post wimp interactive systems based on formal specification, ECEASST, p.69, 2013.

D. Sinnig, P. Chalin, and F. Khendek, Towards a common semantic foundation for use cases and task models, Proceedings of the First International Workshop on Formal Methods for Interactive Systems, vol.183, pp.73-88, 2007.

R. , W. Soukoreff, and I. Mackenzie, Theoretical upper and lower bounds on typing speed using a stylus and a soft keyboard, Behaviour & Information Technology, vol.14, issue.6, pp.370-379, 1995.

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

I. O. , Standardization. ISO 9241-11: Ergonomic Requirements for Office Work with Visual Display Terminals (VDTs): Part 11: Guidance on Usability, 1998.

L. Su, H. Bowman, and P. Barnard, Performance of reactive interfaces in stimulus rich environments, applying formal methods and cognitive frameworks, Proceedings of the 2nd International Workshop on Formal Methods for Interactive Systems, vol.208, pp.95-111, 2008.

H. Thimbleby and A. Gimblett, Dependable keyed data entry for interactive systems, vol.45, 2011.

J. Turner, J. Bowen, and S. Reeves, Using Abstraction with Interaction Sequences for Interactive System Modelling, STAF 2018 Collocated Workshops, pp.257-273, 2018.

M. Westergaard, A game-theoretic approach to behavioural visualisation, Proceedings of the 2nd International Workshop on Formal Methods for Interactive Systems, vol.208, pp.113-129, 2008.