nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Refinement Based Formal Development of Human-Machine Interface

verfasst von : Romain Geniet, Neeraj Kumar Singh

Erschienen in: Software Technologies: Applications and Foundations

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Human factors have been considered as the most common causes of accidents, particularly for interacting with complex critical systems related to avionics, railway, nuclear and medical domains. Mostly, a human-machine interface (HMI) is developed independently and the correctness of possible interactions is heavily dependent on testing, which cannot guarantee the absence of run-time errors. The use of formal methods in HMI development may assure such guarantee. This paper presents a methodology for developing an HMI using a correct by construction approach, which allows us to introduce the HMI components, functional behaviour and the required safety properties progressively. The proposed methodology, generic refinement strategy, supports a development of the model-view-controller (MVC) architecture. The whole approach is formalized using Event-B and relies on the Rodin tools to check the internal consistency with respect to the given safety properties, invariants and events. Finally, an industrial case study is used to illustrate the effectiveness of our proposed approach for developing an HMI.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Towards Handling Latency in Interactive Software

Nächstes Kapitel Using Abstraction with Interaction Sequences for Interactive System Modelling

http://singh.perso.enseeiht.fr/Conference/FMIS2018/HMI_Models.zip.

https://tel.archives-ouvertes.fr/file/index/docid/48279/filename/2_2modelesinterface_referen.html

Abowd, G.D., Wang, H.M., Monk, A.F.: A formal technique forautomated dialogue development. In: Proceedings of the 1st Conference on Designing Interactive Systems: Processes, Practices, Methods, & Techniques, DIS 1995, pp. 219–226. ACM, New York (1995)

Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)CrossRef

Abrial, J.R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, New York (2010)CrossRef

Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in event-b. Int. J. Softw. Tools Technol. Transf. 12(6), 447–466 (2010)CrossRef

Ameur, Y.A.: Cooperation of formal methods in an engineering based software development process. In: 2000 Proceedings Second International Conference Integrated Formal Methods, IFM 2000, Dagstuhl Castle, Germany, 1–3 November, pp. 136–155 (2000)

Ameur, Y.A., Aït-Sadoune, I., Mota, J., Baron, M.: Validation et vérification formelles de systèmes interactifs multi-modaux fondées sur la preuve. In: Proceedings of the 18th International Conference of the Association Francophone d’Interaction Homme-Machine, Montreal, Quebec, Canada, 18–21 April 2006, pp. 123–130 (2006)

Ameur, Y.A., Girard, P., Jambon, F.: A uniform approach for specification and design of interactive systems: the B method. In: Design, Specification and Verification of Interactive Systems 1998, Supplementary Proceedings of the Fifth International Eurographics Workshop, 3–5 June 1998, Abingdon, United Kingdom, pp. 51–67 (1998)

Ameur, Y.A., Girard, P., Jambon, F.: Using the B formal approach for incremental specification design of interactive systems. In: Engineering for Human-Computer Interaction, IFIP TC2/TC13 WG2.7/WG13.4 Seventh Working Conference on Engineering for Human-Computer Interaction, Heraklion, Crete, Greece, 14–18 September, pp. 91–109 (1998)

10.

Ameur, Y.A., Sadoune, I.A., Baron, M.: Etude et comparaison de scénarios de développements formels d’interfaces multi-modales fondés sur la preuve et le raffinement. RSTI- Ingénierie des Systèmes d’Informations 13(2), 127–155 (2008)CrossRef

11.

Baron, M., Lucquiaud, V., Autard, D., Scapin, D.L.: K-made: Unenvironnement pour le noyau du modèle de description del’activité. In: Proceedings of the 18th Conference onL’Interaction Homme-Machine, IHM 2006, pp. 287–288. ACM, New York (2006)

12.

Bolton, M.L., Siminiceanu, R.I., Bass, E.J.: A systematic approach to model checking human - automation interaction using task analytic models. IEEE Trans. Syst. Man Cybern. - Part A: Syst. Hum. 41(5), 961–976 (2011)CrossRef

13.

Bolton, M.L., Bass, E.J.: Building a formal model of a human-interactive system: insights into the integration of formal methods and human factors engineering. In: First NASA Formal Methods Symposium - NFM, California, USA, 6–8 April, pp. 6–15 (2009)

14.

Bowen, J., Reeves, S.: Formal models for user interface design artefacts. Innov. Syst. Softw. Eng. 4(2), 125–141 (2008)CrossRef

15.

Bowen, J., Reeves, S.: Refinement for user interface designs. Electron. Notes Theor. Comput. Sci. 208, 5–22 (2008)CrossRef

16.

Campos, J.C., Harrison, M.D.: Systematic analysis of control panel interfaces using formal tools. In: Graham, T.C.N., Palanque, P. (eds.) DSV-IS 2008. LNCS, vol. 5136, pp. 72–85. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-70569-7_6CrossRef

17.

Combéfis, S., Giannakopoulou, D., Pecheur, C., Feary, M.: Learning system abstractions for human operators. In: Proceedings of the International Workshop on Machine Learning Technologies in Software Engineering, MALETS 2011, pp. 3–10. ACM, New York City (2011)

18.

Combéfis, S., Pecheur, C.: A bisimulation-based approach to the analysis of human-computer interaction. In: Proceedings of the 1st ACM SIGCHI Symposium on Engineering Interactive Computing Systems, EICS 2009, pp. 101–110. ACM, New York (2009)

19.

Coutaz, J., Nigay, L., Salber, D., Blandford, A., May, J., Young, R.M.: Four easy pieces for assessing the usability of multimodal interaction: the care properties. In: Nordby, K., Helmersen, P., Gilmore, D.J., Arnesen, S.A. (eds.) Human-Computer Interaction. IFIP Advances in Information and Communication Technology, pp. 115–120. Springer, Boston (1995). https://doi.org/10.1007/978-1-5041-2896-4_19CrossRef

20.

Dix, A., Finlay, J.E., Abowd, G.D., Beale, R.: Human-Computer Interaction, 3rd edn. Prentice-Hall Inc., Upper Saddle River (2003)MATH

21.

EB2ALL: An automatic code generation tool from Event-B (2011). http://eb2all.loria.fr/

22.

Eijk, P.V., Diaz, M. (eds.): Formal Description Technique Lotos: Results of the Esprit Sedos Project. Elsevier Science Inc., New York (1989)MATH

23.

Heymann, M., Degani, A.: Formal analysis and automatic generation of user interfaces: approach, methodology, and an algorithm. Hum. Factors 49(2), 311–330 (2007)CrossRef

24.

Jambon, F.: From formal specifications to secure implementations. In: Proceedings of the Fourth International Conference on Computer-Aided Design of User Interfaces III, Valenciennes, France, 15–17 May 2002, pp. 51–62 (2002)CrossRef

25.

Lecrubier, V.: A formal language for designing, specifying and verifying critical embedded human machine interfaces. Theses, INSTITUT SUPERIEUR DE L’AERONAUTIQUE ET DE L’ESPACE (ISAE); UNIVERSITE DE TOULOUSE, June 2016. https://hal.archives-ouvertes.fr/tel-01455466

26.

Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45236-2_46CrossRef

27.

Li, M., Wei, J., Zheng, X., Bolton, M.L.: A formal machine-learning approach to generating human-machine interfaces from task models. IEEE Trans. Hum.-Mach. Syst. 47(6), 822–833 (2017)CrossRef

28.

Méry, D., Singh, N.K.: Automatic code generation from event-b models. In: Proceedings of the Second Symposium on Information and Communication Technology, SoICT 2011, pp. 179–188. ACM, New York (2011)

29.

Mohand Oussaïd, L.M.O.: Formal modelling and verification of multimodal human computer interfaces : output multimodality. Theses, ISAE-ENSMA Ecole Nationale Supérieure de Mécanique et d’Aérotechique - Poitiers, December 2014. https://tel.archives-ouvertes.fr/tel-01127547

30.

Navarre, D., Palanque, P., Paternò, F., Santoro, C., Bastide, R.: A tool suite for integrating task and system models through scenarios. In: Johnson, C. (ed.) DSV-IS 2001. LNCS, vol. 2220, pp. 88–113. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45522-1_6CrossRefMATH

31.

Palanque, P., Bastide, R., Sengès, V.: Validating interactive system design through the verification of formal task and system models. In: Bass, L.J., Unger, C. (eds.) EHCI 1995. IFIP Advances in Information and Communication Technology, pp. 189–212. Springer, Boston (1996). https://doi.org/10.1007/978-0-387-34907-7_11CrossRef

32.

Palanque, P.A., Bastide, R.: Petri net based design of user-driven interfaces using the interactive cooperative objects formalism. In: Paternó, F. (ed.) Interactive Systems: Design, Specification, and Verification Focus on Computer Graphics (Tutorials and Perspectives in Computer Graphics), pp. 383–400. Springer, Berlin (1995). https://doi.org/10.1007/978-3-642-87115-3_23CrossRef

33.

Palanque, P., Bastide, R.: Verification of an interactive software by analysis of its formal specification. In: Nordby, K., Helmersen, P., Gilmore, D.J., Arnesen, S.A. (eds.) Human—Computer Interaction. IFIP Advances in Information and Communication Technology, pp. 191–196. Springer, Boston (1995). https://doi.org/10.1007/978-1-5041-2896-4_32CrossRef

34.

Reenskaug, T.M.H.: The original MVC reports (1979)

35.

Ruksenas, R., Masci, P., Harrison, M.D., Curzon, P.: Developing and verifying user interface requirements for infusion pumps: a refinement approach. ECEASST, 69 (2013). ISSN: 1863-2122

36.

Pinheiro da Silva, P., Griffiths, T., Paton, N.W.: Generating user interface code in a model based user interface development environment. In: Proceedings of the Working Conference on Advanced Visual Interfaces, AVI 2000, pp. 155–160. ACM, New York (2000)

37.

Singh, N.K.: Using Event-B for Critical Device Software Systems. Springer, Heidelberg (2013)CrossRef

Titel: Refinement Based Formal Development of Human-Machine Interface
verfasst von: Romain Geniet
Neeraj Kumar Singh
Verlag: Springer International Publishing
Buch: Software Technologies: Applications and Foundations
Print ISBN: 978-3-030-04770-2

Electronic ISBN: 978-3-030-04771-9

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-030-04771-9_19

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"