J. R. Abrial, Modeling in Event-B: System and Software Engineering, 2010.

J. R. Abrial, M. Butler, S. Hallerstede, T. S. Hoang, F. Mehta et al., Rodin: An open toolset for modelling and reasoning in event-b, Int. J. Softw. Tools Technol. Transf, vol.12, issue.6, pp.447-466, 2010.

Y. Aït-ameur, Cooperation of formal methods in an engineering based software development process, Integrated Formal Methods, Second International Conference, IFM 2000, pp.136-155, 2000.

Y. Ait-ameur, I. Ait-sadoune, and M. Baron, Etude et comparaison de scénarios de développements formels d'interfaces multi-modales fondés sur la preuve et le raffinement, Informations, vol.13, issue.2, pp.127-155, 2008.

Y. Aït-ameur, P. Girard, and F. Jambon, Using the B formal approach for incremental specification design of interactiv systems, IFIP TC2/TC13 WG2.7/WG13.4 Seventh Working Conference on Engineering for Human-Computer Interaction, pp.91-109, 1998.

, ARINC 661-2: Prepared by Airlines Electronic Engineering Committee. Cockpit Display System Interfaces to User Systems, Arinc Specification, pp.661-663, 2005.

;. B. Ausbourg, G. Durrieu, and P. Roché, Deriving a formal model of an interactive system from its UIL description in order to verify and to test its behaviour, Proceedings of the Eurographics Workshop DSV-IS'96, 1996.

B. Ausbourg(d'), Using Model Checking for the Automatic Validation of User Interfaces Systems, Design, Specification and Verification of Interactive Systems '98. Eurographics, 1998.

E. Barboni, C. Martinie, D. Navarre, P. A. Palanque, and M. Winckler, Bridging the gap between a behavioural formal description technique and a user interface description language: Enhancing ICO with a graphical user interface markup language, SCP, vol.86, pp.3-29, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01119843

M. L. Bolton, R. I. Siminiceanu, and E. J. Bass, A systematic approach to model checking human -automation interaction using task analytic models, IEEE Transactions on Systems, Man, and Cybernetics -Part A: Systems and Humans, vol.41, issue.5, pp.961-976, 2011.

J. C. Campos and M. D. Harrison, Systematic Analysis of Control Panel Interfaces Using Formal Tools, pp.72-85, 2008.

S. Chatty, M. Magnaudet, and D. Prun, Verification of properties of interactive components from their executable code, Proceedings of the 7th ACM SIGCHI Symposium on Engineering Interactive Computing Systems, pp.276-285, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01619784

P. Curzon, P. Masci, P. Oladimeji, R. Ruk??nas, H. Thimbleby et al., Human-Computer Interaction and the Formal Certification and Assurance of Medical Devices: The CHI+MED Project, 2nd Workshop on Verification and Assurance (Verisure2014), in association with Computer-Aided Verification (CAV), 2014.

. Formedicis-project,

N. Ge, A. Dieumegard, E. Jenn, B. Ausbourg, and Y. Aït-ameur, Formal development process of safety-critical embedded human machine interface systems, 11th International Symposium on Theoretical Aspects of Software Engineering, TASE'17, pp.1-8, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01740640

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

N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud, The synchronous dataflow programming language Lustre, Proceedings of IEEE, pp.1305-1320, 1991.

M. D. Harrison, P. Masci, J. C. Campos, and P. Curzon, Verification of user interface software: The example of use-related safety requirements and programmable medical devices, IEEE Trans. Human-Machine Systems, vol.47, issue.6, pp.834-846, 2017.

F. Jambon, From formal specifications to secure implementations, Computer-Aided Design of User Interfaces III, Proceedings of the Fourth International Conference on Computer-Aided Design of User Interfaces, pp.51-62, 2002.

V. ;. Lecrubier, . Institut-superieur-de-l'aeronautique, and . De-l'espace, A formal language for designing, specifying and verifying critical embedded human machine interfaces. Theses
URL : https://hal.archives-ouvertes.fr/tel-01455466

. Universite-de-toulouse, , 2016.

M. Leuschel and M. Butler, ProB: A Model Checker for B, LNCS, pp.855-874, 2003.

B. A. Myers, Why are human-computer interfaces difficult to design and implement? Tech. rep, 1993.

D. Navarre, R. Bastide, and P. Palanque, A tool-supported design framework for safety critical interactive systems, Interacting with Computers, vol.15, issue.3, pp.309-328, 2003.

D. Navarre, P. A. Palanque, F. Paternò, C. Santoro, and R. Bastide, A tool suite for integrating task and system models through scenarios, 8th International Workshop on Interactive Systems: Design, Specification, and Verification (DSV-IS), pp.88-113, 2001.

P. Palanque, R. Bastide, and V. Sengès, Validating interactive system design through the verification of formal task and system models, pp.189-212, 1996.

P. A. Palanque and R. Bastide, Petri net based design of user-driven interfaces using the interactive cooperative objects formalism. In: Design, Specification and Verification of Interactive Systems, Proc. of the First International Eurographics Workshop, pp.383-400, 1994.

P. A. Palanque, J. Ladry, D. Navarre, and E. Barboni, High-fidelity prototyping of interactive systems can be formal too, Human-Computer Interaction. New Trends, 13th International Conference, HCI International, pp.667-676, 2009.

F. Paterno, C. Mancini, and S. Meniconi, ConcurTaskTrees: A Diagrammatic Notation for Specifying Task Models, pp.362-369, 1997.

B. Shneiderman, C. Plaisant, M. Cohen, S. Jacobs, and N. Elmqvist, Designing the User Interface -Strategies for Effective Human-Computer Interaction, 2016.