CURATe Measures for Human-Integrated Systems: A Model Checking Approach

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.