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 CURATerelatedspecifications 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 CURATemeasures with respect to a broader range of human-integrated system elements: the interface, includingdocumentation, configurable hardware, and control units; the user, including capabilities, actions, and knowledge;the device, including automation, actuators, and transducers; and the environment, including stimuliand constraints that could shape behavior. We describe a concept for what elements/interactions among themneed to be modeled formally as well as a concept for applicable CURATe specifications. With respect tothese concepts, we propose a formal model architecture and one temporal logic encoding for each CURATespecification.
展开▼
