A Formal Method for Evaluating the Performance Level of Human-Human Collaborative Procedures

  • Dan Pan
  • Matthew L. BoltonEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9180)


Human-human interaction is critical to safe operations in domains like nuclear power plants (NPP) and air transportation. Usually collaborative procedures and communication protocols are developed to ensure that relevant information is correctly heard and actions are correctly executed. Such procedures should be designed to be robust to miscommunications between humans. However, these procedures can be complex and thus fail in unanticipated ways. To address this, researchers have been investigating how formal verification can be used to prove the robustness of collaborative procedures to miscommunications. However, previous efforts have taken a binary approach to assessing the success of such procedures. This can be problematic because some failures may be more desirable than others. In this paper, we show how specification properties can be created to evaluate the level of success of a collaborative procedure formally. We demonstrate the capability of these properties to evaluate a realistic procedure for a NPP application.


Formal method Human communication Human error 


  1. 1.
    Bass, E.J., Bolton, M.L., Feigh, K., Griffith, D., Gunter, E., Mansky, W., Rushby, J.: Toward a multi-method approach to formalizing human-automation interaction and human-human communications. In: 2011 IEEE International Conference on Systems, Man, and Cybernetics, pp. 1817–1824 (2011)Google Scholar
  2. 2.
    Bolton, M.L.: Model checking human-human communication protocols using task models and miscommunication generation. J. Aerosp. Comput. Inf. Commun. doi: 10.2514/1.I010276. (in press, 2015)
  3. 3.
    Bolton, M.L., Bass, E.J., Siminiceanu, R.I.: Using formal verification to evaluate human-automation interaction: A review. IEEE Trans. Syst. Man, Cyberne.: Syst. 43(3), 488–503 (2013)CrossRefGoogle Scholar
  4. 4.
    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)CrossRefGoogle Scholar
  5. 5.
    Clarke, E.M., Wing, J.M.: Formal methods: state of the art and future directions. ACM Comput. Surv. (CSUR) 28(4), 626–643 (1996)CrossRefGoogle Scholar
  6. 6.
    Connell, L.: Pilot and controller communication issues. In: Methods and Metrics of Voice Communication, pp. 19–27 (1996)Google Scholar
  7. 7.
    Dong, X.: Influence of Human-system Interface Design Method and Time Pressure on Human Error. Master thesis. Tsinghua University, Beijing, China (2010)Google Scholar
  8. 8.
    Hirotsu, Y., Suzuki, K., Kojima, M., Takano, K.: Multivariate analysis of human error incidents occurring at nuclear power plants: several occurrence patterns of observed human errors. Cogn. Technol. Work 3(2), 82–91 (2001)CrossRefGoogle Scholar
  9. 9.
    MacDonald, P.E., Shah, V.N., Ward, L.W., Ellison, P.G.: Steam generator tube failures. NUREG/CR-6365, INEL-95/0393. Nuclear Regulatory Commission, Washington, DC, United States (1996)Google Scholar
  10. 10.
    Murphy, P.: The role of communications in accidents and incidents during rail possessions. In: Engineering Psychology and Cognitive Ergonomics, vol. 5, pp. 447–454 (2001)Google Scholar
  11. 11.
    Paternò, F., Santoro, C., Tahmassebi, S.: Formal models for cooperative tasks: concepts and an application for en-route air traffic control. In: Markopoulos, P., Johnson, P. (eds.) Proceedings of the 5th International Conference on Design, Specification, and Verification of Interactive Systems, pp. 71–86. Springer, Vienna (1998)Google Scholar
  12. 12.
    Strater, O.: Investigation of communication errors in nuclear power plants. Communication in High Risk Environments. Linguistische Berichte, Sonderheft 12, 155–179 (2003)Google Scholar
  13. 13.
    Traum, D., Dillenbourg, P.: Miscommunication in multi-modal collaboration. In: AAAI Workshop on Detecting, Repairing, And Preventing Human–Machine Miscommunication, pp. 37–46 (1996)Google Scholar
  14. 14.
    Wilson, R.M., Runciman, W.B., Gibberd, R.W., Harrison, B.T., Newby, L., Hamilton, J.D.: The quality in Australian health care study. Med. J. Aust. 163(9), 458–471 (1995)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  1. 1.Department of Industrial EngineeringTsinghua UniversityBeijingPeople’s Republic of China
  2. 2.Department of Industrial and Systems EngineeringUniversity at Buffalo, State University of New YorkAmherstUSA

Personalised recommendations