To support safe and effective human-system integration, a safety-critical system should be Complete, Understandable, Robust, Accurate, and Time efficient (CURATe) with respect to the user, interface, device, and environmental context. Using highly automated model checkers, researchers have shown that CURATe-related specifications can be verified early in the design process for a subset of system elements and interactions. This research introduces an extended model checking approach that aims to address all CURATe measures with respect to a broader range of human-integrated system elements: the interface, including documentation, configurable hardware, and control units; the user, including capabilities, actions, and knowledge; the device, including automation, actuators, and transducers; and the environment, including stimuli and constraints that could shape behavior. We describe a concept for what elements/interactions among them need to be modeled formally as well as a concept for applicable CURATe specifications. With respect to these concepts, we propose a formal model architecture and one temporal logic encoding for each CURATe specification.
References
1.
AbbateA. J.BassE. J. (2017). Modeling affordance using formal methods. In Proceedings of the 2017 Annual Meeting of the Human Factors and Ergonomics Society (pp. 723–727). SAGE Publications.
2.
BarwiseJ.PerryJ. (1981). Situations and attitudes. The Journal of Philosophy, 668–691.
3.
BoltonM. L.BassE. J.SiminiceanuR. I. (2013). Using formal verification to evaluate human-automation interaction: A review. Systems, Man, and Cybernetics: Systems, IEEE Transactions on, 43(3), 488–503.
4.
BoltonM. L.SiminiceanuR. I.BassE. J. (2011). A systematic approach to model checking human-automation interaction using task analytic models. Systems, Man and Cybernetics, Part A: Systems and Humans, IEEE Transactions on, 41(5), 961–976.
5.
ClarkeE. M.EmersonE. A.SistlaA. P. (1986). Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems (TOPLAS), 8(2), 244–263.
6.
ClarkeE. M.GrumbergO.PeledD. A. (1999). Model Checking. Cambridge, MA, USA: MIT Press.
7.
HussmannH.MeixnerG.ZuehlkeD. (2011). Model-Driven Development of Advanced User Interfaces. Berlin, Germany: Springer Science & Business Media.
ISO. (2008). ISO/IEC 26514:2008: Systems and software engineering– Requirements for designers and developers of user documentation. Geneva, Switzerland.
10.
ISO. (2015). ISO/IEC 62366-1:2015: Medical devices – Part 1: Application of usability engineering to medical devices. Geneva.
11.
ISO. (2017). ISO 9241-125:2017: Ergonomics of human-system interaction – Part 125: Guidance on visual presentation of information. Geneva, Switzerland.
12.
RukšėnasR.BackJ.CurzonP.BlandfordA. (2008). Formal modelling of salience and cognitive load. Electronic Notes in Theoretical Computer Science, 208, 57–75.
13.
RukšėnasR.CurzonP.BackJ.BlandfordA. (2007). Formal modelling of cognitive interpretation. In Proceedings of the 13th International Workshop on Design, Specification, and Verification of Interactive Systems (pp. 123–136). Springer.
14.
WeyersB.BowenJ.DixA.PalanqueP. (2017). In WeyersB.BowenJ.DixA.PalanqueP. (Eds.), The Handbook of Formal Methods in Human-Computer Interaction (chap. State of the Art on Formal Methods for Interactive Systems). New York, NY: Springer.
