Model checking is increasingly being used with task analytic behavior models to prove whether models of human-interactive systems are safe and reliable. Such methods could be used to predict how different types of users will choose to use system features. However, existing methods focus on modeling the full space of possible human behaviors without considering how users will choose to navigate this space. In this work, we present a new approach that enables model checking to predict how different types of users will use features of an interactive system by employing a novel combination of task analytic modeling and utility theory. This paper presents this method and illustrates its power with a smart thermostat application. The results of the application analysis and its implications for future research are discussed.
References
1.
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.
2.
AmmannP.OffuttJ. (2016). Introduction to software testing. Cambridge University Press.
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.
BoltonM. L. (2015). Model checking human–human communication protocols using task models and miscommunication generation. Journal of Aerospace Information Systems, 12(7), 476–489.
5.
BoltonM. L. (2017a). Novel developments in formal methods for human factors engineering. In Proceedings of the human factors and ergonomics society annual meeting (pp. 715–717). Atlanta: Sage.
6.
BoltonM. L. (2017b). A task-based taxonomy of erroneous human behavior. International Journal of Human-Computer Studies, 108, 105–121.
7.
BoltonM. L.BassE. J. (2009). 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.
8.
BoltonM. L.BassE. J. (2013). Generating erroneous human behavior from strategic knowledge in task models and evaluating its impact on system safety with model checking. IEEE Transactions on Systems, Man and Cybernetics: Systems, 43(6), 1314–1327.
9.
BoltonM. L.BassE. J. (2017). Enhanced operator function model (eofm): A task analytic modeling formalism for including human behavior in the verification of complex systems. In WeyersB.BowenJ.DixA.PalanqueP. (Eds.), The handbook of formal methods in human-computer interaction (pp. 343–377). Cham: Springer International.
10.
BoltonM. L.BassE. J.SiminiceanuR. I. (2012). Generating phenotypical erroneous human behavior to evaluate human-automation interaction using model checking. International Journal of Human-Computer Studies, 70(11), 888–906.
11.
BoltonM. L.BassE. J.SiminiceanuR. I. (2013). Using formal verification to evaluate human-automation interaction in safety critical systems, a review. IEEE Transactions on Systems, Man and Cybernetics: Systems, 43(3), 488–503.
12.
BoltonM. L.SiminiceanuR. I.BassE. J. (2011). A systematic approach to model checking human-automation interaction using task-analytic models. IEEE Transactions on Systems, Man, and Cybernetics, Part A, 41(5), 961–976.
13.
BoltonM. L.ZhengX.MolinaroK.HouserA.LiM. (2017). Improving the scalability of formal human-automation interaction verification analyses that use task-analytic models. Innovations in Systems and Software Engineering, 13(1), 1–17.
14.
CalinescuR.KwiatkowskaM. (2009). Using quantitative analysis to implement autonomic it systems. In Software engineering, 2009. icse 2009. ieee 31st international conference on (pp. 100–110).
15.
CámaraJ.GarlanD.SchmerlB.PandeyA. (2015). Optimal planning for architecture-based self-adaptation via model checking of stochastic games. In Proceedings of the 30th annual ACM symposium on applied computing (pp. 428–435).
16.
ChuR. W.MitchellC. M.JonesP. M. (1995). Using the operator function model and OFMspert as the basis for an intelligent tutoring system: Towards a tutor/aid paradigm for operators of supervisory control systems. IEEE Transactions on Systems, Man and Cybernetics Part A: Systems and Humans, 25(7), 1054–1075.
17.
ClarkeE. M.GrumbergO.PeledD. A. (1999). Model checking. Cambridge: MIT Press.
18.
CookseyR. W. (1996). Judgment analysis: Theory, methods, and applications. Academic Press.
19.
de MouraL.OwreS.RueßH.RushbyJ.ShankarN.SoreaM.TiwariA. (2004). SAL 2. In Proceedings of the 16th international conference on computer aided verification (pp. 496–500). Springer.
20.
de MouraL.OwreS.ShankarN. (2003). The SAL language manual (Tech. Rep. No. CSL-01-01). Menlo Park: Computer Science Laboratory, SRI International.
21.
EmersonE. A. (1990). Temporal and modal logic. In van LeeuwenJ.MeyerA. R.NivatM.PatersonM.PerrinD. (Eds.), Handbook of theoretical computer science (pp. 995–1072). Cambridge: MIT Press.
22.
FieldsR. E. (2001). Analysis of erroneous actions in the design of critical systems (Unpublished doctoral dissertation). University of York, York.
23.
GintisH. (2014). The bounds of reason: Game theory and the unification of the behavioral sciences. Princeton University Press.
24.
GrumbergO.VeithH. (2008). 25 years of model checking: History, achievements, perspectives. Berlin: Springer.
25.
ISO. (2005). Ergonomics of the thermal environment – analytical determination and interpretation of thermal comfort using calculation of the pmv and ppd indices and local thermal comfort criteria (ISO standard no.).
26.
KirwanB.AinsworthL. K. (1992). A guide to task analysis. London: Taylor and Francis.
27.
LecerofA.PaternòF. (1998). Automatic support for usability evaluation. IEEE Transactions on Software Engineering, 24(10), 863–888.
28.
LeeJ.MorayN. (1992). Trust, control strategies and allocation of function in human-machine systems. Ergonomics, 35(10), 1243–1270.
29.
LiM.BoltonM. L. (ND). Automated test case generation for human-machine interaction. (Under Review)
30.
LiM.WeiJ.ZhengX.BoltonM. L. (2017). A formal machine learning approach to generating human-machine interfaces from task models. IEEE Transactions on Human-Machine Systems, 47, 822–833.
31.
LomuscioA.StruloB.WalkerN. G.WuP. (2010). Model checking optimisation based congestion control algorithms. Fundamenta Informaticae, 102(1), 77–96.
32.
PanD.BoltonM. L. (2018). Properties for formally assessing the performance level of human-human collaborative procedures with miscommunications and erroneous human behavior. International Journal of Industrial Ergonomics, 63, 75-88.
33.
PaternòF. (2000). Model-based design of interactive applications. Intelligence, 11(4), 26–38.
34.
PaternòF.SantoroC. (2001). Integrating model checking and HCI tools to help designers verify user interface properties. In Proceedings of the 7th International Workshop on the Design, Specification, and Verification of Interactive Systems (pp. 135–150). Berlin: Springer.
35.
SykesD.HeavenW.MageeJ.KramerJ. (2010). Exploiting non-functional preferences in architectural adaptation for self-managed systems. In Proceedings of the 2010 acm . . . .
36.
Von NeumannJ.MorgensternO. (1953). Theory of games and economic behavior. Princeton University Press.
37.
WeyersB.BowenJ.DixA.PalanqueP. (Eds.). (2017). The handbook of formal methods in human-computer interaction. Berlin: Springer.
38.
WingJ. M. (1990). A specifier’s introduction to formal methods. Computer, 23(9), 8, 10–22, 24.
