Breakdowns in complex systems often occur as a result of system elements interacting in ways unanticipated by analysts or designers. In systems with human operators, human-automation interaction associated with both normative and erroneous human behavior can contribute to such failures. This paper presents a method for automatically generating task analytic models encompassing both erroneous and normative human behavior from normative task models. The resulting model can be integrated into a formal system model so that system safety properties can be formally verified with a model checker. This allows analysts to prove that a human automation-interactive system (as represented by the model) will or will not satisfy safety properties with both normative and generated erroneous human behavior. This method is illustrated with a case study: the operation of a radiation therapy machine. In this example, a problem resulting from a generated erroneous human action is discovered. Future extensions of our method are discussed.
Get full access to this article
View all access options for this article.
References
1.
AbowdG. D.WangH.MonkA. F. (1995). A formal technique for automated dialogue development. In Proceedings of the 1st Conference on Designing Interactive Systems (pp. 219–226). New York: ACM.
2.
Aït-AmeurY.BaronM. (2006). Formal and experimental validation approaches in HCI systems design based on a shared event B model. International Journal on Software Tools for Technology Transfer, 8(6), 547–563.
3.
BastideR.BasnyatS. (2007). Error patterns: Systematic investigation of deviations in task models. In Task models and diagrams for users interface design (pp. 109–121). Berlin: Springer.
4.
BogdanichW. (2010, January 23). The radiation boom: Radiation offers new cures, and ways to do harm. The New York Times.
5.
BoltonM. L. (2010). Using task analytic behavior modeling, erroneous human behavior generation, and formal methods to evaluate the role of human-automation interaction in system failure. Unpublished doctoral dissertation, University of Virginia, Charlottesville.
6.
BoltonM. L.BassE. J. (2009a). Enhanced operator function model: A generic human task behavior modeling language. In Proceedings of the IEEE International Conference on Systems Man and Cybernetics (pp. 2983–2990). Piscataway: IEEE.
7.
BoltonM. L.BassE. J. (2009b). A method for the formal verification of human interactive systems. In Proceedings of the 53rd Annual Meeting of the Human Factors and Ergonomics Society (pp. 764–768). Santa Monica: Human Factors and Ergonomics Society.
8.
BoltonM. L.BassE. J. (2010). Formally verifying human-automation interaction as part of a system model: Limitations and tradeoffs. Innovations in Systems and Software Engineering: A NASA Journal. doi: 10.1007/s11334-010-0129-9.
9.
BoltonM. L.BassE. J. (in press). Using task analytic models to visualize model checker counterexamples. In Proceedings of the IEEE International Conference on Systems Man and Cybernetics. Piscataway: IEEE.
10.
BoltonM. L.SiminiceanuR. I.BassE. J. (n.d.). A systematic approach to model checking human-automation interaction using task-analytic models. Under review.
11.
BrederekeJ.LankenauA. (2005). Safety-relevant mode confusions–modelling and reducing them. Reliability Engineering and System Safety, 88(3), 229–245.
12.
CamposJ. C.HarrisonM. D. (2008). Systematic analysis of control panel interfaces using formal tools. In Proceedings of the 15th International Workshop on the Design, Verification and Specification of Interactive Systems (pp. 72–85). Berlin: Springer.
13.
ClarkeE. M.GrumbergO.PeledD. A. (1999). Model checking. Cambridge: MIT Press.
14.
CurzonP.RukšėnasR.BlandfordA. (2007). An approach to formal verification of humanücomputer interaction. Formal Aspects of Computing, 19(4), 513–550.
15.
DeganiA.HeymannM. (2002). Formal verification of human-automation interaction. Human Factors, 44(1), 28–43.
16.
De MouraL.OwreS.ShankarN. (2003). The SAL language manual (Tech. Rep. No. CSL-01-01). Menlo Park: Computer Science Laboratory, SRI International.
17.
FieldsR. E. (2001). Analysis of erroneous actions in the design of critical systems. Unpublished doctoral dissertation, University of York, York.
18.
HollnagelE. (1993a). Human reliability analysis: Context and control. Academic Press.
19.
HollnagelE. (1993b). The phenotype of erroneous actions. International Journal of Man-Machine Studies, 39(1), 1–32.
20.
JonesP. M. (1997). Human error and its amelioration. In Handbook of systems engineering and management (pp. 687–702). Malden: Wiley.
21.
LevesonN. G.TurnerC. S. (1993). An investigation of the therac-25 accidents. Computer, 26(7), 18–41.
22.
LindsayP.ConnellyS. (2002). Modelling erroneous operator behaviours for an air-traffic control task. In Proceedings of the 3rd Australasian User Interface Conference (Vol. 7, p. 43–54). Melbourne: ACS.
23.
MitchellC. M.MillerR. A. (1986). A discrete control model of operator function: A methodology for information dislay design. IEEE Transactions on Systems Man Cybernetics Part A: Systems and Humans, 16(3), 343–357.
24.
ReasonJ. (1990). Human error. New York: Cambridge University Press.
25.
SheridanT. B.ParasuramanR. (2005). Human-automation interaction. Reviews of human factors and ergonomics, 1(1), 89–129.
26.
WingJ. M. (1990). A specifier's introduction to formal methods. Computer, 23(9), 8, 10–22, 24.
