Verification templates for the analysis of user interface software design

The paper describes templates for model-based analysis of usability and safety aspects of user interface software design. The templates crystallize general usability principles commonly addressed in user-centred safety requirements, such as the ability to undo user actions, the visibility of operational modes, and the predictability of user interface behavior. These requirements have standard forms across different application domains, and can be instantiated as properties of specific devices. The modeling and analysis process is carried out using the Prototype Verification System (PVS), and is further facilitated by structuring the specification of the device using a format that is designed to be generic across interactive systems. A concrete case study based on a commercial infusion pump is used to illustrate the approach. A detailed presentation of the automated verification process using PVS shows how failed proof attempts provide precise information about problematic user interface software features.This work has been funded by the EPSRC research grant EP/G059063/1: CHI+ MED (Computer-Human Interaction for Medical Devices). We are grateful to Harold Thimbleby's team at Swansea University, part of the CHI+ MED project, and especially Patrick Oladimeji who developed the infusion pump simulation that helped us develop the models. We also thank the anonymous reviewers for valuable feedback. Jose C. Campos and Paolo Masci were funded by project NORTE-01-0145-FEDER-000016, financed by the North Portugal Regional Operational Programme (NORTE 2020), under the PORTUGAL 2020 Partnership Agreement, and through the European Regional Development Fund (ERDF)