Masci P, Oladimeji P, Zhang Y, Jones P, Curzon P, Thimbleby H.  2015.  PVSio-web 2.0: Joining PVS to Human-Computer Interaction. 27th International Conference on Computer Aided Verification (CAV2015). Lecture Notes in Computer Science, vol 9206, 2015. Abstractpvsioweb-cav2015.pdf

PVSio-web is a graphical environment for facilitating the design and evaluation of interactive (human-computer) systems. Using PVSio-web, one can generate and evaluate realistic interactive prototypes from formal models. PVSio-web has been successfully used over the last two years for analyzing commercial, safety-critical medical devices. It has been used to create training material for device developers and device users. It has also been used for medical device design, by both formal methods experts and non-technical end users.

This paper presents the latest release of PVSio-web 2.0, which will be part of the next PVS distribution. The new tool architecture is discussed, and the rationale behind its design choices are presented

Masci P, Couto LD, Larsen PG, Curzon P.  2015.  Integrating the PVSio-web modelling and prototyping environment with Overture. 13th Overture Workshop, satellite event of FM2015. Abstractpvsioweb-overture2015.pdf

Tools are needed that overcome the barriers preventing development teams using formal verification technologies. We present our work integrating PVSio-web with the Overture development and analysis environment for VDM. PVSio-web is a graphical environment for modelling and prototyping interactive systems. Prototypes developed within PVSio-web can closely resemble the visual appearance and behaviour of a real system. The behaviour of the prototypes is entirely driven by executable formal models. These formal models can be generated automatically from Emucharts, graphical diagrams based on the Statechart notation. Emucharts conveniently hides aspects of the formal syntax that create barriers for developers and domain experts who are new to formal methods. Here, we present the implementation of a VDM-SL model generator for Emucharts. An example is presented based on a medical device. It demonstrates the benefits of using Emucharts to develop a formal model, how PVSio-web can be used to perform lightweight formal analysis, and how the developed VDM-SL model generator can be used to produce a model that can be further analysed within Overture.

Masci P, Mallozzi P, DeAngelis FL, Serugendo GDM, Curzon P.  2015.  Using PVSio-web and SAPERE for rapid prototyping of user interfaces in Integrated Clinical Environments. Verisure2015, Workshop on Verification and Assurance, co-located with CAV2015. Abstractpvsioweb-sapere-verisure2015.pdf

Integrated clinical environments (ICEs) consist of interoperable medical devices that seamlessly exchange data and commands to create safety interlocks and closed loop controls to improve the quality of care delivered to the patient. Currently at the prototype stage, they promise to form the basis of a new generation of healthcare systems for high acuity patients. Regulators such as the US Food and Drug Administration are promoting the development of tools and techniques for verification and validation of essential safety requirements for ICEs. To date, little research has focused on the certification and assurance of their user interfaces with respect to use errors. In this work, we demonstrate how the PVSio-web prototyping tool can be conveniently used in combination with the communication framework SAPERE to generate realistic ICE systems prototypes from formal models. This approach is particularly suitable for exploring requirements, design, and regulatory issues of usability and safety of the user interfaces of ICE systems. An example ICE system prototype is presented, along with an example analysis demonstrating how the prototype can be used to explore subtle user interface design issues that could lead to usability and safety hazards in clinical scenarios.

Masci P, Oladimeji P, Mallozzi P, Curzon P, Thimbleby H.  2015.  PVSio-web: mathematically based tool support for the design of interactive and interoperable medical systems. 5th EAI International Conference on Wireless Mobile Communication and Healthcare - "Transforming healthcare through innovations in mobile and wireless technologies". Abstractmobihealth-pvsioweb.pdf

Use errors, where medical devices work to specification but lead to the clinicians making mistakes resulting in patient harm, is a critical problem. Manufacturers need tools to help them find such design flaws at an early stage and regulators need tools to help check devices are safe to approve for market. We have developed a prototyping tool, PVSio-web, to help check the safety of medical device interface and interaction design. It supports a model-based design process: that is, it is based on precise mathematical descriptions of the device's behaviour. This allows sophisticated proof and model checking technology to be used to verify that devices meet essential safety requirements. The architecture allows for the flexible addition of `plug-in' modules to extend its functionality giving different views of the design that allow different stakeholders to work together. Working with the US regulator, the Food and Drug Administration (FDA), our tool has helped identify problems in a series of commercial medical devices. Hospitals have used it as part of training programmes highlighting safety-related design issues. In ongoing work we are developing plug-ins that support the verification and validation of interoperable medical systems.

Masci P, Curzon P, Thimbleby H.  2015.  Early identification of software causes of use-related hazards in medical devices. 5th EAI International Conference on Wireless Mobile Communication and Healthcare - "Transforming healthcare through innovations . Abstractmobihealth-hazard-analysis.pdf

A hazard is a potential source of physical injury or damage to people or environment, and a hazard analysis is the process of identifying all known and foreseeable hazards and their causes in a system. In this paper, we illustrate our ongoing work in collaboration with the FDA on defining a hazard analysis technique for early identification of the causes in user interface software design of use-related hazards. The technique integrates human cognitive process models and general interaction design principles, and uses a model-based approach for systematic exploration of potential hazards. Preliminary experiments suggest that this hazard analysis technique can substantially improve the identification of use-related hazards at the early stages of software design as compared to standard hazard analysis techniques.

Bernardeschi C, Domenici A, Masci P.  2015.  Towards a Formalization of System Requirements for an Integrated Clinical Environment. 5th EAI International Conference on Wireless Mobile Communication and Healthcare - "Transforming healthcare through innovations in mobile and wireless technologies". mobihealth-requirements.pdf
Oladimeji P, Thimbleby H, Masci P, Curzon P.  2015.  Issues in number entry user interface styles: Recommendations for mitigation. 5th EAI International Conference on Wireless Mobile Communication and Healthcare - "Transforming healthcare through innovations in mobile and wireless technologies". mobihealth-numbers.pdf
Harrison M, Campos J, Masci P, Curzon P.  2015.  Templates as heuristics for proving properties of medical devices. 5th EAI International Conference on Wireless Mobile Communication and Healthcare - "Transforming healthcare through innovations in mobile and wireless technologies". antennatemplatesv5-final.pdf
Masci P, Zhang Y, Jones P, Curzon P, Thimbleby H.  2014.  Formal Verification of Medical Device User Interfaces Using PVS. Fundamental Approaches to Software Engineering. Lecture Notes in Computer Science (LNCS), vol 8411:200-214. Abstractmasci-fase2014.pdf

We present a formal verification approach for detecting design issues related to user interaction, with a focus on user interface of medical devices. The approach makes a novel use of configuration diagrams proposed by Rushby to formally verify important human factors properties of user interface implementation. In particular, it first translates the software implementation of user interface into an equivalent formal specification, from which a behavioral model is constructed using theorem proving; human factors properties are then verified against the behavioral model; lastly, a comprehensive set of test inputs are produced by exploring the behavioral model, which can be used to challenge the real interface implementation and to ensure that the issues detected in the behavior model do apply to the implementation. We have prototyped the approach based on the PVS proof system, and applied it to analyze the user interface of a real medical device. The analysis detected several interaction design issues in the device, which may potentially lead to severe consequences.

Masci P, Oladimeji P, Curzon P, Thimbleby H.  2014.  Using PVSio-web to demonstrate software issues in medical user interfaces. 4th International Symposium on Foundations of Healthcare Information Engineering and Systems (FHIES2014). Lecture Notes in Computer Science book series (LNCS), volume 9062 Abstractmasci-fhies14.pdf

We have used formal methods technology to investigate software and user interface design issues that may induce use error in medical devices. Our approach is based on mathematical models that capture safety concerns related to the use of a device. We analysed nine commercial medical devices from six manufacturers with our approach, and precisely identified 30 design issues. All identified issues can induce use errors that could lead to adverse clinical consequences, such as numbers being incorrectly entered. An issue with formal approaches is in making results accessible to developers, human factors experts and clinicians. In this paper, we use our tool PVSio-web to demonstrate the identified issues: PVSio-web allows us to generate realistic and interactive user interface prototypes from the same mathematical models used for analysis. Users can explore the behaviour of the prototypes by pressing buttons on realistic user interfaces that reproduce the functionality and visual representation of the real devices. Users can examine the device behaviour resulting from any interaction. Key sequences identified from analysis can be used to explore in detail the identified design issues in an accessible way.

Masci P, Zhang Y, Jones P, Thimbleby H, Curzon P.  2014.  A generic user interface architecture for analyzing use hazards in infusion pump software. Proceedings of Medical Cyber Physical Systems Workshop (MedCPS2014). Abstractmasci-medcps2014.pdf

This paper presents a generic infusion pump user interface (GIP-UI) architecture that intends to capture the common characteristics and functionalities of interactive software incorporated in broad classes of infusion pumps. It is designed to facilitate the identification of use hazards and their causes in infusion pump designs. This architecture constitutes our first e!ort at establishing a model-based risk analysis methodology that helps manufacturers identify and mitigate use hazards in their products at early stages of the development life-cycle. The applicability of the GIP-UI architecture has been confirmed in a hazard analysis focusing on the number entry software of existing infusion pumps, in which the GIP-UI architecture is used to identify a substantial set of user interface design errors that may contribute to use hazards found in infusion pump incidents.

Masci P, Zhang Y, Jones P, Oladimeji P, D'Urso E, Bernardeschi C, Curzon P, Thimbleby H.  2014.  Combining PVSio with Stateflow. Proceedings of the 6th NASA Formal Methods Symposium (NFM2014). Lecture Notes in Computer Science book series (LNCS, volume 8430) Abstractpvsioweb-stateflow-nfm2014.pdf

An approach to integrating PVS executable specifications and Stateflow models is presented that uses web services to enable a seamless exchange of simulation events and data between PVS and Stateflow. Thus, it allows the wide range of applications developed in Stateflow to benefit from the rigor of PVS verification. The effectiveness of the approach is demonstrated on a medical device prototype, which consists of a user interface developed in PVS and a software controller implemented in Stateflow. Simulation on the prototype shows that simulation data produced is exchanged smoothly between in PVSio and Stateflow.

Curzon P, Masci P, Oladimeji P, Ruksenas R, Thimbleby H, D'Urso E.  2014.  Human-Computer Interaction and the Formal Certification and Assurance of Medical Devices: The CHI+MED Project. 2nd Workshop on Verification and Assurance (Verisure2014), in association with Computer-Aided Verification (CAV), part of the Vienna Summer of Logic. Abstractverisure14.pdf

The number of recalls of medical device with embedded computers due to safety issues in recent years suggests there is a need for new approaches to support the process. There is increasing concern about the impact of systematic use errors. There has been little research focusing on model-based tool support for the assurance and certification of medical devices with respect to systematic use error, however. The CHI+MED project ( aims to address this gap. It is concerned with the design of safer medical devices with a specific focus on human-computer interaction. We are developing a range of integrated model-based engineering methods and other formal and semi-formal techniques to support the certification process, both pre- and post-market, including their use in the wider system context. In this position paper we review our approach and the contributions to date.

Bernardeschi C, Domenici A, Masci P.  2014.  Integrated Simulation of Implantable Cardiac Pacemaker Software and Heart Models. Proceedings of the 2nd International Congress on Cardiovascular Technologies. 2014_cardiotechnix.pdf
Harrison M, Masci P, Campos JC, Curzon P.  2013.  Automated theorem proving for the systematic analysis of interactive systems. Proceedings of the 5th International Workshop on Formal Methods for Interactive Systems. Abstractharrisonmcc.pdf

This paper describes the use of an automated theorem prover to analyse properties of interactive behaviour. It offers an alternative to model checking for the analysis of interactive systems. There are situations, for example when demonstrating safety, in which alternative complementary analyses provide assurance to the regulator. The rigour and detail offered by theorem proving makes it possible to explore features of the design of the interactive system, as modelled, beyond those that would be revealed using model checking. Theorem proving can also speed up proof in some circumstances. The paper illustrates how a theory generated as a basis for theorem proving (using PVS) was developed systematically from a MAL model used to model check the same properties. It also shows how the CTL properties used to check the original model can be translated into theorems.