Testing is an effective approach for finding discrepancies between intended and actual system behavior. However, the complexity of modern system can make it difficult for analysts to anticipate all the interactions that need to be tested. This is particularly true for human-interactive systems where humans may do things that were not anticipated by analysts. We address this by introducing a novel approach to automated test case generation for human-machine interaction. We do this by combining formal models of human-machine interfaces with formal models of human task behavior. We then use the robust search capabilities of model checking to generate test sequences guaranteed to satisfy test coverage criteria. We demonstrate the capabilities of our approach with of a pod-based coffee machine. Results and future research are discussed.
Get full access to this article
View all access options for this article.
References
1.
AmmannP.OffuttJ. (2016). Introduction to software testing. Cambridge University Press.
2.
BarbosaA.PaivaA. C.CamposJ. C. (2011). Test case generation from mutated task models. In Proceedings of the 3rd acm sigchi symposium on engineering interactive computing systems (pp. 175–184).
3.
BassE. J.BoltonM. L.FeighK.GriffithD.GunterE.ManskyW.RushbyJ. (2011). Toward a multi-method approach to formalizing human-automation interaction and human-human communications. In Proceedings of the IEEE International Conference on Systems, Man, and Cybernetics (pp. 1817–1824). Piscataway: IEEE.
4.
BertolinoA. (2007). Software testing research: Achievements, challenges, dreams. In 2007 future of software engineering (pp. 85–103). IEEE Computer Society.
5.
BoltonM. L. (2015). Model checking human–human communication protocols using task models and miscommunication generation. Journal of Aerospace Information Systems.
6.
BoltonM. L. (2017a). Novel developments in formal methods for human factors engineering. In Proceedings of the human factors and ergonomics society annual meeting (Vol. 61, pp. 715–717). Los Angeles: Sage.
7.
BoltonM. L. (2017b). A task-based taxonomy of erroneous human behavior. International Journal of Human-Computer Studies, 108, 105–121.
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, 6(3), 219–231.
9.
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.
10.
BoltonM. L.JimenezN.van PaassenM. M.TrujilloM. (2014). Automatically generating specification properties from task models for the formal verification of human-automation interaction. IEEE Transactions on Human-Machine Systems, 44, 561–575.
11.
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.
12.
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.
CamposJ. C.FayollasC.MartinieC.NavarreD. (2016). Systematic automation of scenario-based testing of user interfaces. EICS.
15.
ClarkeE. M.GrumbergO.PeledD. A. (1999). Model checking. Cambridge: MIT Press.
16.
d’AusbourgB. (1998). Using model checking for the automatic validation of user interfaces systems. In Design, specification and verification of interactive systems’98 (pp. 242–260). Springer.
17.
De MouraL.OwreS.ShankarN. (2003). The SAL language manual (Tech. Rep. No. CSL-01-01). Menlo Park: Computer Science Laboratory, SRI International.
18.
FraserG.WotawaF.AmmannP. E. (2009). Testing with model checkers: A survey. Software Testing, Verification and Reliability, 19(3), 215–261.
19.
HamonG.de MouraL.RushbyJ. (2004). Generating efficient test sets with a model checker. In Proceedings of the second international conference on software engineering and formal methods (pp. 261–270). IEEE.
20.
KirwanB.AinsworthL. K. (1992). A guide to task analysis. London: Taylor and Francis.
21.
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, 1– 12.
22.
MemonA. M.PollackM. E.Lou SoffaM. (2001). Hierarchical GUI Test Case Generation Using Automated Planning. IEEE Trans. Software Eng., 27(2), 144–155.
23.
SarterN. B.WoodsD. D. (1995). How in the world did we ever get into that mode? Mode error and awareness in supervisory control. Human Factors, 37(1), 5–19.
24.
VieiraM.LeducJ.HaslingW. M.SubramanyanR.KazmeierJ. (2006). Automation of GUI Testing Using a Model-driven Approach. AST, 9.
