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 (2018, to appear)santone.pdf
Bernardeschi C, Masci P, Caramella D, Dell'Osso R.  2018.  The benefits of using interactive device simulations as training material for clinicians: an experience report with a contrast media injector used in CT. Medical Cyber Physical Systems Workshop 2018. SIGBED Review newsletter (2018, to appear)stellant-v3.pdf
Silva CC, Masci P, Zhang Y, Jones P, Campos JC.  2018.  A Use Error Taxonomy for Improving Human-Machine Interface Design in Medical Devices. Medical Cyber Physical Systems Workshop 2018. SIGBED Review newsletter (2018, to appear)mcps-taxonomy-v3g.pdf
Broccia G, Masci P, Milazzo P.  2018.  Modeling and Analysis of Human Memory Load in Multitasking Scenarios. 10th ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS 2018). Abstract

This paper presents on-going work developing a formal framework for the model-based analysis of human-machine interaction in multiple critical systems. The framework builds on classical results from applied psychology on selective attention and working memory. The framework is intended for developers of interactive critical systems to identify plausible human multitasking strategies that are likely to be adopted by operators when using multiple interactive systems at the same time, and to estimate the memory load necessary to complete concurrent tasks. This type of analysis is especially useful at the early stages of system design, to better understand the effort necessary to operate the system when an implementation or a prototype of the system is unavailable. The analysis can also be used retrospectively, to analyse already implemented systems and complement results from user studies. An example based on infusion pumps, used in chemotherapy to infuse doses over a period, is employed to demonstrate the utility of the framework. The framework makes it possible to model the interactive tasks necessary to configure the pumps and start the infusion. The results of the analysis indicate situations where the operator is unable to carry out the task because of omission errors. These results are in line with experimental results reported in the literature, and may provide more detailed hypotheses that can be validated experimentally.

Masci P, Harrison MD, Campos JC.  2018.  Formal modelling as a component of user centred design. Workshop on Formal Methods for Interactive Systems (FMIS-2018), Springer LNCS, to appear. Abstractfmis18rev2-camera-ready.pdf

User centred design approaches typically focus understanding on context and producing sketch designs. These sketches are often non functional (e.g., paper) prototypes. They provide a means of exploring candidate design possibilities using techniques such as cooperative evaluation. This paper describes a further step in the process using formal analysis techniques. The sketch design of a device is enhanced into a specification that is then analysed using formal techniques, thus providing a systematic approach to checking plausibility and consistency during early design stages. Once analysed, a further prototype is constructed using an executable form of the specification, providing the next candidate for evaluation with potential users. The technique is illustrated through an example based on a pill dispenser.

Anzivino S, Quaini G, Pisetta V, Masci P, Bertoldi A, Nollo G.  2018.  Implementation of a multi-specialized electronic health record for managing cardiological rehabilitation paths. Italian Forum of Ambient Assisted Living (ForItALL). Abstractforitaal_2018_paper_6.pdf

Cardiac Rehabilitation (CR) is an intervention for managing the post-acute phase of the disease.
According to international guidelines, it includes three consecutive phases: the first phase, during
the acute period, in the hospital; the second, during a hospitalization or in outpatient, in order to
evaluate and modify the patient's risk factors; the third, outside the hospital setting, is carried out to
change, support and promote a correct lifestyle. To guarantee that all patients have access to the
most appropriate rehabilitation track, it is necessary to create structured paths on the territory and
under a multi-professional patient monitoring. The elective tool for patient-centered management is
the Integrated Care Pathway (ICP). It is oriented to the communication and integration of all actors
involved in patient’s management, requires the identification of a case manager and a team of
health professionals able to manage complexity and comorbidities, and supports patient
involvement. Care pathways as complex as these can be better supported if traditional paper-
based approaches are transformed into interactive systems that use Information and
Communication Technologies (ICT). The introduction of ICP and ICT implies the reconfiguration of
the clinical record that from a repository of the data becomes a multi-accessible tool for the
management of visits and the visualization of the results of instrumental examinations. In order to
translate this concept in the field of the CR at patient’s home, we created a multi-specialist
electronic health record accessible to both professionals (cardiologist, nurse, dietician,
psychologist, sanitary assistant) that make diagnosis, prescribe therapies and physical exercise,
monitor patient’s parameters, and patients, to allow them to consult therapies and results of clinical
exams. We used Agile Methodology to develop this Medical Device (MD) compliant, by design,
with the European laws on MD, Privacy, and Usability. To avoid malfunctions due
to incorrect or incomplete collection of requirements, and to optimize development time, the Agile
continuous process of revision and brainstorming were performed by applying simulation
technologies [6] that allowed us to accelerate substantially the identification and validation of user
interface requirements and to identify and fix potential functional errors. The virtual prototypes
reproducing the functionalities and the visual appearance of the system were subjected to the CR’s
multidisciplinary team of Azienda Provinciale per i Servizi Sanitari di Trento (professionals,
engineers, etc.) involved in the project during several “sprint phases” as an alternative tool to the
static mock-ups. All this led to the implementation of a MD validated by design.

Palmieri M, Bernardeschi C, Masci P.  2018.  A Flexible Framework for FMI-based Co-Simulation of Human-Centred Cyber-Physical Systems. 2nd Workshop on Formal Co-Simulation of Cyber-Physical Systems (CoSim-CPS-18), Springer LNCS, 2018 (to appear). Abstractcosim-cps-18_paper_4-full.pdf

This paper presents our on-going work on developing a flexible framework for formal co-simulation of human-centred cyber-physical systems. The framework builds on and extends an existing prototyping toolkit, adding novel functionalities for automatic generation of user interface prototypes equipped with a standard FMI-2 co-simulation interface. The framework is developed in JavaScript, and uses a flexible templating mechanism for converting stand-alone device prototypes into Functional Mockup Units (FMUs) capable of exchanging commands and data with any FMI-compliant co-simulation engine. Two concrete examples are presented to demonstrate the capabilities of the framework.

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


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.