Publications

Harrison M, Masci P, Campos JC, Curzon P.  2017.  The Specification and Analysis of Use Properties of a Nuclear Control System. The Handbook of Formal Methods in Human-Computer Interaction. Abstractp-00m-t6a.pdf

The chapter explores a layered approach to the analysis of the Nuclear Power Plant Control System described in Chapter 4. A model is specified to allow the analysis of use-centred properties based on generic templates. User interface properties include: the visibility of state attributes, the clarity of the mode structure and the ease with which an action can be recovered from. Property templates are used as heuristics to ease the construction of requirements for the control system interface.

Ruksenas R, Masci P, Curzon P.  2016.  Developing and Verifying User Interface Requirements for Infusion Pumps: A Refinement Approach. From Action Systems to Distributed Systems: The Refinement Approach. wp325.pdf
Bernardeschi C, Masci P, Santone A.  2018.  Data Leakage in Java applets with Exception Mechanism. Proceedings of Italian Conference on Cyber-Security (ITASEC18). CEUR Workshop Proceedings, to appearsantone.pdf
Harrison M, Masci P, Campos JC, Curzon P.  2017.  Demonstrating that medical devices satisfy user related safety requirements. Software Engineering in Healthcare (FHIES/SEHC 2014). 9062 Abstractharrison-fhies14.pdf

One way of contributing to a demonstration that a medical device is acceptably safe is to show that the device satisfies a set of requirements known to mitigate hazards. This paper describes experience using formal techniques to model an IV infusion device and to prove that the modelled device captures a set of requirements. The requirements chosen for the study are based on a draft proposal developed by the US Food and Drug Administration (FDA). A major contributor to device related errors are (user) interaction errors. For this reason the chosen models and requirements focus on user interface related issues.

Fayollas C, Martinie C, Palanque P, Masci P, Harrison M, Campos JC, Silva SR.  2017.  Evaluation of formal IDEs for human-machine interface design and analysis: the case of CIRCUS and PVSio-web. Proceedings of the Third Workshop on Formal Integrated Development Environment. 240:1-19. Abstract1701.08465.pdf

n/a

Masci P, Zhang Y, Jones P, Campos JC.  2017.  A Hazard Analysis Method for Systematic Identification of Safety Requirements for User Interface Software in Medical Devices. 15th International Conference on Software Engineering and Formal Methods (SEFM 2017). LNCS, volume 10469, Springer Abstractsefm17-cameraready.pdf

Formal methods technologies have the potential to verify the usability and safety of user interface (UI) software design in medical devices, enabling significant reductions in use errors and consequential safety incidents with such devices. This however depends on comprehensive and verifiable safety requirements to leverage these techniques for detecting and preventing flaws in UI software that can induce use errors. This paper presents a hazard analysis method that extends Leveson's System Theoretic Process Analysis (STPA) with a comprehensive set of causal factor categories, so as to provide developers with clear guidelines for systematic identification of use-related hazards associated with medical devices, their causes embedded in UI software design, and safety requirements for mitigating such hazards. The method is evaluated with a case study on the Gantry-2 radiation therapy system, which demonstrates that 1) as compared to standard STPA, our method allowed us to identify more UI software design issues likely to cause use-related hazards; and 2) the identified UI software design issues facilitated the definition of precise, verifiable safety requirements for UI software, which could be readily formalized in verification tools such as Prototype Verification System (PVS).

Harrison MD, Drinnan M, Campos JC, Masci P, Freitas L, Di Maria C, Whitaker M.  2017.  Safety analysis of software components of a dialysis machine using model checking. 14th International Conference on Formal Aspects of Component Software. Springer Lecture Notes in Computer Science (LNCS) vol. 10487 Abstractpaper_7.pdf

The paper describes the practical use of a model checking technique to contribute to the risk analysis of a new paediatric dialysis machine. The formal analysis focuses on one component of the system, namely the table-driven software controller which drives the dialysis cycle and deals with error management. The analysis provided evidence of the verification of risk control measures relating to the software component. The paper describes the productive dialogue between the developers of the device, who had no experience or knowledge of formal methods, and an analyst who had experience of using the formal analysis tools. There were two aspects to this dialogue. The first concerned the translation of safety requirements so that they preserved the meaning of the requirement. The second involved understanding the relationship between the software component under analysis and the broader concern of the system as a whole. The paper focuses on the process, highlighting how the team recognised the advantages over a more traditional testing approach.

Palmieri M, Bernardeschi C, Masci P.  2017.  Co-simulation of semi-autonomous systems: the Line Follower Robot case study. 1st Workshop on Formal Co-Simulation of Cyber-Physical Systems (CoSim-CPS), LNCS Springer. 10729 Abstractcosim-cps-17_paper_4.pdf

Semi-autonomous systems are capable of sensing their environment and perform their tasks autonomously, but they may also be supervised by humans. The shared manual/automatic control makes the dynamics of such systems more complex, and undesirable and hardly predictable behaviours can arise from human-machine interaction. When these systems are used in critical applications, such as autonomous driving or robotic surgery, the identification of conditions that may lead the system to violate safety requirements is of main concern, since people actually entrust their life on them. In this paper, we extend an FMI-based co-simulation framework for cyber-physical systems with the possibility of modelling semi-autonomous robots. Co-simulation can be used to gain more insights on the system under analysis at early stages of system development, and to highlight the impact of human interaction on safety. This approach is applied to the Line Follower Robot case study, available in the INTO-CPS project.

Pinto M, Goncalves M, Masci P, Campos JC.  2017.  TOM: a Model-Based GUI Testing framework. 14th International Conference on Formal Aspects of Component Software. 10487 Abstractpaper_25.pdf

Applying model-based testing to interactive systems enables the systematic testing of the system by automatically simulating user actions on the user interface. It reduces the cost of (expensive) user testing by identifying implementations errors without the involvement of human users, but raises a number of specific challenges, such as how to achieve good coverage of the actual use of the system during the testing process. This paper describes TOM, a model-based testing framework that uses a combination of tools and mutation testing techniques to maximize testing of user interface behaviors

Bernardeschi C, Domenici A, Masci P.  2016.  Modeling Communication Network Requirements for an Integrated Clinical Environment in the Prototype Verification System. ICTS4eHealth - 1st IEEE Workshop on ICT solutions for eHealth. Abstractmasci-icts4ehealth-cr.pdf

Health care practices increasingly rely on complex technological infrastructure, and new approaches to the integration of information and communication technology in those practices lead to the development of such concepts as integrated clinical environments and smart intensive care units. These concepts refer to hospital settings where therapy relies heavily on inter-operating medical devices, supervised by clinicians assisted by advanced monitoring and coordinating software. In order to ensure safety and effectiveness of patient care, it is necessary to specify the requirements of such socio-technical systems in the most rigorous and precise way. This paper presents an approach to the formalization of system requirements for communication networks deployed in integrated clinical environment, based on the higher-order logic language of a theorem-proving environment, the Prototype Verification System. http://dx.doi.org/10.1109/ISCC.2016.7543728

Fayollas C, Martinie C, Palanque P, Masci P, Harrison MD, Campos JC, Silva SR.  2016.  Evaluation of formal IDEs for human-machine interface design and analysis: the case of CIRCUS and PVSio-web. Workshop on Integrated Formal Development Environment (F-IDE 2016), co-located with FM2016. f-ide2016-camera-ready.pdf
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. https://doi.org/10.1007/978-3-319-21690-4_30 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.