Abstract
Several modern safety-critical environments involve multiple humans interacting not only with automation, but also between themselves in complex ways. For example, in handling the National Airspace, we have moved from the traditional single controller sitting in front of a display to multiple controllers interacting with their individual display, possibly each other’s displays, and other more advanced automated systems. To evaluate safety in such contexts, it is imperative to include the role of one or multiple human operators in our analysis, as well as focus on properties of human automation interactions. This chapter discusses two novel frameworks developed at NASA for the design and analysis of human–machine interaction problems. The first framework supports modeling and analysis of automated systems from the point of view of their human operators and supports the specification and verification of HMI-specific properties such as mode confusion, controllability, or whether operator tasks are compatible with a particular system. The second framework captures the complexity of modern HMI systems by taking a multi-agent approach to modeling and analyzing multiple human agents interacting with each other as well as with automation.
The original version of the book was revised: For detailed information please see Erratum. The erratum to the book is available at 10.1007/978-3-319-51838_21
An erratum to this chapter can be found at http://dx.doi.org/10.1007/978-3-319-51838-1_21
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
The mental model is commonly referred to as conceptual model (Johnson and Henderson 2002) in the literature, that is, an abstraction of the system which outlines what the operator can do with the system and what she needs in order to interact with it.
- 2.
The subscript M for the system refers to Machine and the subscript U for the mental model refers to User.
References
Ameur YA, Boniol F, Wiels V (2010) Toward a wider use of formal methods for aerospace systems design and verification. Int J Softw Tools Technol Transf 12(1):1–7. ISSN 1433-2779. doi:10.1007/s10009-009-0131-4
Bastide R, Navarre D, Palanque P (2003) A tool-supported design framework for safety critical interactive systems. Interact Comput 15(3):309–328
Bolton M, Siminiceanu R, Bass E (2011) 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
Bolton M, Bass E (2010) Using task analytic models and phenotypes of erroneous human behavior to discover system failures using model checking. In: Proceedings of the 54th annual meeting of the human factors and ergonomics society, pp 992–996
Bolton M, Bass E, Siminiceanu R (2008) Using formal methods to predict human error and system failures. In: Proceedings of the second international conference on applied human factors and ergonomics (AHFE 2008)
Bovair Susan, Kieras DE, Polson PG (1990) The acquisition and performance of text-editing skill: a cognitive complexity analysis. Hum Comput Interact 5(1):1–48
Bratman M (1987) Intention, plans, and practical reason
Bredereke J, Lankenau A (2002) A rigorous view of mode confusion. In: Proceedings of the 21st international conference on computer safety, reliability and security (SAFECOMP 2002). Springer, pp 19–31, Sept 2002
Bredereke J, Lankenau A (2005) Safety-relevant mode confusions–modelling and reducing them. Reliab Eng Syst Saf 88(3):229–245
Butterworth R, Blandford A (1997) Programmable user models: the story so far. Middlesex University, London
Campos JC, Harrison MD (2008) Systematic analysis of control panel interfaces using formal tools. In: Nicholas Graham TC, Palanque PA (eds) Proceedings of the 15th international workshop on design, specification and verification of interactive systems (DSV-IS 2008), vol 5136. Springer, Lecture notes in computer science, pp 72–85
Campos JC, Harrison MD (2011) Model checking interactor specifications. Autom Softw Eng 8(3):275–310
Clancey WJ, Sachs P, Sierhuis M, Van Hoof R (1998) Brahms: simulating practice for work systems design. Int J Hum Comput Stud 49(6):831–865
Combéfis S (2009) Operational model: integrating user tasks and environment information with system model. In: Proceedings of the 3rd international workshop on formal methods for interactive systems, pp 83–86
Combéfis S (2013) A formal framework for the analysis of human-machine interactions. PhD thesis, Université catholique de Louvain
Combéfis S, Giannakopoulou D, Pecheur C (2016) Automatic detection of potential automation surprises for ADEPT models. IEEE Trans Hum Mach Syst Spec Issue Syst Approaches Hum Mach Interface Improv Resil Robust Stab 46(2):
Combéfis S, Giannakopoulou D, Pecheur C, Feary M (2011) A formal framework for design and analysis of human-machine interaction. In: Proceedings of the IEEE international conference on systems, man and cybernetics, Anchorage, Alaska, USA, 9–12 Oct 2011. IEEE, pp 1801–1808. ISBN 978-1-4577-0652-3. doi:10.1109/ICSMC.2011.6083933
Combéfis S, Pecheur C (2009) A bisimulation-based approach to the analysis of human-computer interaction. In: Calvary G, Nicholas Graham TC, Gray P (eds) Proceedings of the ACM SIGCHI symposium on engineering interactive computing systems (EICS’09)
Curzon P, Rukšėnas R, Blandford A (2007) An approach to formal verification of human-computer interaction. Formal Aspects Comput 19(4):513–550
Feary MS (2010) A toolset for supporting iterative human—automation interaction in design. Technical Report 20100012861, NASA Ames Research Center, March 2010
Godefroid P (1997) Model checking for programming languages using verisoft. In: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on principles of programming languages. ACM, pp 174–186
Heymann M, Degani A (2007) Formal analysis and automatic generation of user interfaces: approach, methodology, and an algorithm. Hum Factors: J Hum Factors Ergon Soc 49(2):311–330
Hunter J, Raimondi F, Rungta N, Stocker R (2013) A synergistic and extensible framework for multi-agent system verification. In: Proceedings of the 2013 international conference on autonomous agents and multi-agent systems. International Foundation for Autonomous Agents and Multiagent Systems, pp 869–876
JavaPathfinder (JPF) (2016). http://babelfish.arc.nasa.gov/trac/jpf/
Javaux D (2002) A method for predicting errors when interacting with finite state systems. How implicit learning shapes the user’s knowledge of a system. Reliab Eng Syst Saf 75:147–165
Johnson J, Henderson A (2002) Conceptual models: begin by designing what to design. Interactions 9:25–32
Lee PU, Smith NM, Homola J, Brasil C, Buckley N, Cabrall C, Chevalley E, Parke B, Yoo HS (2015) Reducing departure delays at laguardia airport with departure-sensitive arrival spacing (dsas) operations. In: Eleventh USA/Europe air traffic management research and development seminar (ATM)
Leveson NG, Turner CS (1993) Investigation of the therac-25 accidents. IEEE Comput 26(7):18–41
Miller SP, Whalen MW, Cofer DD (2010) Software model checking takes off. Commun ACM 53(2):58–64. ISSN 0001-0782. doi:10.1145/1646353.1646372
Navarre D, Palanque P, Bastide R (2001) Engineering interactive systems through formal methods for both tasks and system models. In Proceedings of the RTO Human Factors and Medicine Panel (HFM) specialists’ meeting, pp 20.1–20.17, June 2001
Rungta N, Brat G, Clancey WJ, Linde C, Raimondi F, Seah C, Shafto M (2013) Aviation safety: modeling and analyzing complex interactions between humans and automated systems. In: Proceedings of the 3rd international conference on application and theory of automation in command and control systems. ACM, pp 27–37
Rungta N, Mercer EG, Raimondi F, Krantz BC, Stocker R, Wallace A (2016) Modeling complex air traffic management systems. In: Proceedings of the 8th international workshop on modeling in software engineering. ACM, pp 41–47
Rushby JM (2011) New challenges in certification for aircraft software. In: Chakraborty S, Jerraya A, Baruah SK, Fischmeister S (eds) EMSOFT. ACM, pp 211–218. ISBN 978-1-4503-0714-7
Sierhuis M (2001) Modeling and simulating work practice. BRAHMS: a multiagent modeling and simulation language for work system analysis and design. PhD thesis, Social Science and Informatics (SWI), University of Amsterdam, SIKS Dissertation Series No. 2001-10, Amsterdam, The Netherlands
Thimbleby H (2010) Press on: principles of interaction programming. The MIT Press, Jan 2010. ISBN 0262514230
Thimbleby H, Gow J (2007) Applying graph theory to interaction design. In Gulliksen J, Harning MB, Palanque P, van der Veer G, Wesson J (eds) Proceedings of the engineering interactive systems joint working conferences EHCI, DSV-IS, HCSE (EIS 2007). Lecture notes in computer science, vol 4940, pp 501–519. Springer, Mar 2007
Tretmans J (2008) Model based testing with labelled transition systems. In: Hierons R, Bowen J, Harman M (eds) Formal methods and testing. Lecture notes in computer science, vol 4949. Springer, pp 1–38
uberlingeng (2004) Investigation Report AX001-1-2/02. Technical report, German Federal Bureau of Aircraft Accidents Investigation
Yasmeen A, Gunter EL (2011) Automated framework for formal operator task analysis. In Dwyer MB, Tip F (eds) ISSTA. ACM, pp 78–88
Young RM, Green TRG, Simon T (1989) Programmable user models for predictive evaluation of interface designs. In: ACM SIGCHI bulletin, vol 20. ACM, pp 15–19
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this chapter
Cite this chapter
Brat, G., Combéfis, S., Giannakopoulou, D., Pecheur, C., Raimondi, F., Rungta, N. (2017). Formal Analysis of Multiple Coordinated HMI Systems. In: Weyers, B., Bowen, J., Dix, A., Palanque, P. (eds) The Handbook of Formal Methods in Human-Computer Interaction. Human–Computer Interaction Series. Springer, Cham. https://doi.org/10.1007/978-3-319-51838-1_15
Download citation
DOI: https://doi.org/10.1007/978-3-319-51838-1_15
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-51837-4
Online ISBN: 978-3-319-51838-1
eBook Packages: Computer ScienceComputer Science (R0)