Proving Use Requirements of Interactive Systems with Remote Monitoring and Control Capabilities

A generation of interoperable devices is emerging in control systems. Devices can be controlled by users at multiple levels. The devices that are controlled may be certified as safe by their vendors, but new issues may arise from their integration and remote use, as new interaction pathways will be enabled that are simply not possible when the device is used as a stand-alone system. This paper is concerned with modelling concrete interfaces that are designed to enable use of these systems. It builds on previous work concerned with proving use-centred safety properties across the interoperable system. The concern of this paper however is describing the relationship between an abstract model and a concrete interface that reflects more concretely the tasks that the users are intended to perform. In the example used in this paper, a menu interface is built on top of the abstract interface. The primary concern of the paper is describing the relationship between the abstract interface and the specified concrete interface. Properties of the interface that were discussed in previous work are proved of the concrete interface. This paper uses, as an example, use-centred safety properties of integrated clinical environments for remote medical care. Four properties are considered briefly: consistency, completeness, feedback and reversibility with an understanding of the tasks that users may perform. More detail will be given to the first two with a particular focus on the relation between the abstract interaction model and a concrete menu based model. The properties are formalised in the language of the PVS verification system. They are mechanically verified using the PVS proof assistant for a model of a realistic prototype of an integrated clinical environment. The presented analysis is intended to be performed during system design and development, and before the actual system is deployed, to increase confidence that the design complies with important use-centred safety properties that capture design guidelines discussed in usability engineering standards. It is envisaged that such an analysis could help inform a safety assessment of the integrated system.