Conference Papers

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. 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. 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). 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. 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). 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
Harrison M, Masci P, Campos JC, Curzon P.  2014.  Demonstrating that medical devices satisfy user related safety requirements. FHIES/SEHC - Fourth Symposium on Foundations of Health Information Engineering and Systems (FHIES) and the Software Engineering in Healthcare (SEHC) - post-proceedings. 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.

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. 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). 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 (http://www.chi-med.ac.uk) 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.

Masci P, Ayoub A, Curzon P, Harrison M, Lee I, Sokolsky O, Thimbleby H.  2013.  Verification of interactive software for medical devices: PCA infusion pumps and FDA regulation as an example. Proceedings ACM Symposium Engineering Interactive Systems - EICS. :81-90. Abstractmascietal.pdf

Medical device regulators such as the US Food and Drug Administration (FDA) aim to make sure that medical devices are reasonably safe before entering the market. To expedite the approval process and make it more uniform and rigorous, regulators are considering the development of reference models that encapsulate safety requirements against which software incorporated into medical devices must be verified. Safety, insofar as it relates to interactive systems and its regulation, is generally a neglected topic, particularly in the context of medical systems.

An example is presented that illustrates how the interactive behaviour of a commercial Patient Controlled Analgesia (PCA) infusion pump can be verified against a reference model. Infusion pumps are medical devices used in healthcare to deliver drugs to patients, and PCA pumps are particular infusion pump devices that are often used to provide pain relief to patients on demand. The reference model encapsulates the Generic PCA safety requirements provided by the FDA, and the verification is performed using a refinement approach.

The contribution of this work is that it demonstrates a concise and semantically unambiguous approach to representing what a regulator’s requirements for a particular interactive device might be, in this case focusing on user-interface requirements. It provides an inspectable and repeatable process for demonstrating that the requirements are satisfied. It has the potential to replace the considerable documentation produced at the moment by a succinct document that can be subjected to careful and systematic analysis.

Oladimeji P, Masci P, Curzon P, Thimbleby H.  2013.  PVSio-web: a tool for rapid prototyping device user interfaces in PVS. FMIS2013, 5th International Workshop on Formal Methods for Interactive Systems, London, UK, June 24, 2013. 69 Abstractfmis2013.pdf

We present PVSio-web which extends the simulation component of the PVS proof system with functionalities for rapid prototyping device user interfaces. The tool presents itself as a classic image-editing environment with functionalities such as area selection and hyperlink creation, thus reducing the barriers that prevent non-experts in formal methods from using PVS. Designers load a picture of the layout of the device user interface under development, specify interactive areas over the layout, and link them to a PVS specification. They can then explore the behaviour of the formal user interface specification through point-and-click interactions. The architecture of the tool is general, and can be used as the basis for extending other verification tools. A demonstration of the capabilities of PVSio-web is presented through an example based on a commercial medical device user interface. Our ultimate aim is to promote and facilitate the use of formal verification tools when developing device user interfaces.

Ruksenas R, Masci P, Harrison M, Curzon P.  2013.  Developing and Verifying User Interface Requirements for Infusion Pumps: A Refinement Approach. FMIS2013, 5th International Workshop on Formal Methods for Interactive Systems, London, UK, June 24, 2013. 69 Abstract964-2899-1-pb.pdf

It is common practice in the description of criteria for the acceptable safety of systems for the regulator to describe safety requirements that should be satisfied by the system. These requirements are typically described precisely but in natural language and it is often unclear how the regulator can be assured that the given requirements are satisfied. This paper is concerned with a rigorous refinement process that demonstrates that a precise requirement is satisfied by the specification of a given device. It focuses on a particular class of requirements that relate to the user interface of the device. For user interface requirements, refinement is made more complex by the fact that systems can use different interaction devices that have very different characteristics. The described refinement process recognises an input/output hierarchy.

Masci P, Ayoub A, Curzon P, Lee I, Sokolsky O, Thimbleby H.  2013.  Model-Based Development of the Generic PCA Infusion Pump User Interface Prototype in PVS. Computer Safety, Reliability, and Security. 8153:228-240. Abstractgpcaui-safecomp2013.pdf

A realistic user interface is rigorously developed for the US Food and Drug Administration (FDA) Generic Patient Controlled Analgesia (GPCA) pump prototype. The GPCA pump prototype is intended as a realistic workbench for trialling development methods and techniques for improving the safety of such devices. A model-based approach based on the use of formal methods is illustrated and implemented within the Prototype Verification System (PVS) verification system. The user interface behaviour is formally specified as an executable PVS model. The specification is verified with the PVS theorem prover against relevant safety requirements provided by the FDA for the GPCA pump. The same specification is automatically translated into executable code through the PVS code generator, and hence a high fidelity prototype is then developed that incorporates the generated executable code.

Harrison M, Campos JC, Masci P, Thomas N.  2012.  Modelling and systematic analysis of interactive systems. Proceedings of the Workshop on Formal Methods in Human-Machine Interaction (Formal H). :25-28. Abstractformalh.2012.proceedings.pdf

Two aspects of our research concern the application of formal methods in human-computer interaction. The first aspect is the modelling and analysis of interactive devices with a particular emphasis on the user device dyad. The second is the modelling and analysis of ubiquitous systems where there are many users, one might say crowds of users.The common thread of both is to articulate and prove properties of interactive systems, to explore interactive behaviour as it influences the user, with a particular emphasis on interaction failure. The goal is to develop systematic techniques that can be packaged in such a way that they can be used effectively by developers. This “whitepaper” will briefly describe the two approaches and their potential value as well as their limitations and development opportunities.

Masci P, Furniss D, Curzon P, Harrison M, Blandford A.  2012.  Supporting Field Investigators with PVS: A Case Study in the Healthcare Domain. Software Engineering for Resilient Systems. 7527:150-164. Abstractmascipvsdistributed.pdf

This paper reports the lessons learnt about the benefits of using a formal verification tool like PVS to support field studies. The presentation is based on a field study in the healthcare domain which was designed to investigate the resilience of human behaviour in an oncology ward of a hospital. The automated reasoning tool PVS was used systematically to compare actual practice observed during the field study with normative behaviour described for example by user manuals for the devices involved. The approach helped (i) identify latent situations that could lead to hazard, and (ii) suggest situations likely to warrant further investigation as part of the field study. The main contribution of this paper is a set of detailed examples that illustrate how we used PVS during the field study, and how the tool led to insights.

Masci P, Huang H, Curzon P, Harrison M.  2012.  Using PVS to Investigate Incidents through the Lens of Distributed Cognition. NASA Formal Methods. 7226:273-278. Abstractmascinasa.pdf

A systematic tool-based method is outlined that raises questions about the circumstances surrounding an incident: why it happened and what went wrong. The approach offers a practical and systematic way to apply a distributed cognition perspective to incident investigations, focusing on how available information resources (or the lack of them) may shape user action, rather than just on causal chains. This perspective supports a deeper understanding of the more systemic causes of incidents. The analysis is based on a higher order-logic model describing how information resources may have influenced the actions of those involved in the incident. The PVS theorem proving system is used to identify situations where available resources may afford unsafe user actions. The method is illustrated using a healthcare case study.

Cauchi A, Gimblett A, Thimbleby HW, Curzon P, Masci P.  2012.  Safer "5-key" number entry user interfaces using differential formal analysis. BCS HCI. :29-38. Abstract

Differential formal analysis is a new user interface analytic evaluation method based on stochastic user simulation. The method is particularly valuable for evaluating safety critical user interfaces, which often have subtle programming issues. The approach starts with the identification of operational design features that define the design space to be explored. Two or more analysts are required to analyse all combinations of design features by simulating keystroke sequences containing keying slip errors. Each simulation produces numerical values that rank the design combinations on the basis of their sensitivity to keying slip errors. A systematic discussion of the simulation results is performed for assessing the causes of any discrepancy, either in numerical values or rankings. The process is iterated until outcomes are agreed upon. In short, the approach combines rigorous simulation of user slip errors with diversity in modelling and analysis methods.

Although the method can be applied to other types of user interface, it is demonstrated through a case study of 5-key number entry systems, which are a common safety critical user interface style found in many medical infusion pumps and elsewhere. The results uncover critical design issues, and are an important contribution of this paper since the results provide device manufacturers guidelines to update their device firmware to make their devices safer.

Masci P, Ruksenas R, Huang H, Curzon P, Harrison M.  2012.  Formal verification and the prevention of systematic user error. FormalH, Workshop on Formal Methods in Human-Machine Interaction sponsored by the IFIP Working Group 13.5 on Human Error, Safety, and System Development.
Bernardeschi C, Cassano L, Domenici A, Masci P.  2011.  A Tool for Signal Probability Analysis of FPGA-Based Systems. COMPTOOLS2011, the 2nd Intl. Conf. on Computational Logics, Algebras, Programming, Tools, and Benchmarking.
Blandford A, Cauchi A, Curzon P, Eslambolchilar P, Furniss D, Gimblett A, Huang H, Lee P, Li Y, Masci P et al..  2011.  Comparing Actual Practice and User Manuals: A Case Study Based on Programmable Infusion Pumps. Eics4Med, the 1st International Workshop on Engineering Interactive Computing Systems for Medicine and Health Care. Abstract

We report on a case study investigating current practice in the use of a programmable infusion pump. We start by formalising an existing description of the procedure followed by nurses for setting up a commercial infusion pump obtained via observation and interview. We then compare and contrast this procedure with a formal description of the sequence of actions reported in the pump's user manual. Mismatches were validated by a training manager. The aim of this comparison is to point out how minor mismatches between the two descriptions can be used to reveal major safety issues. Our contributions are: first, we analyse a real-world system and show the importance of having a clear and consistent specification of the procedures; second, we show how a graph-based notation can be conveniently used for building non-ambiguous and intuitive specifications. We argue that this can provide support to an investigator when building a description of actual practice in that it can help focus attention on areas to observe more closely and questions to ask to understand why procedures, as followed, are the way they are.

Cauchi A, Curzon P, Eslambolchilar P, Gimblett A, Huang H, Lee P, Li Y, Masci P, Oladimeji P, Ruksenas R et al..  2011.  Towards Dependable Number Entry for Medical Devices. Eics4Med, the 1st International Workshop on Engineering Interactive Computing Systems for Medicine and Health Care. Abstract

Number entry is an ubiquitous task in medical devices, but is implemented in many different ways, from decimal keypads to seemingly simple up/down buttons. Operator manuals often do not give clear and complete explanations, and all approaches have subtle variations, with details varying from device to device. This paper explores the design issues, critiques designs, and shows that methods have advantages and disadvantages, particularly in terms of undetected error rates.

Masci P, Curzon P, Blandford A, Furniss D.  2011.  On formalising interactive number entry on infusion pumps. ECEASST. 45 Abstract

We define the predictability of a user interface as the property that an idealised user can predict with sufficient certainty the effect of any action in a given state in a system, where state information is inferred from the perceptible output of the system. In our definition, the user is not required to have full knowledge of a history of actions from an initial state to the current state. Typically such definitions rely on cognitive and knowledge assumptions; in this paper we explore the notion in the situation where the user is an idealised expert and understands perfectly how the device works. In this situation predictability concerns whether the user can tell what state the device is in and accurately predict the consequences of an action from that state simply by looking at the device; normal human users can certainly do no better. We give a formal definition of predictability in higher order logic and explore how real systems can be verified against the property. We specify two real number entry interfaces in the healthcare domain (drug infusion pumps) as case studies of predictable and unpredictable user interfaces. We analyse the specifications with respect to our formal definition of predictability and thus show how to make unpredictable systems predictable.

Masci P, Martinucci M, Giandomenico FD.  2011.  Towards Automated Dependability Analysis of Dynamically Connected Systems. Proceedings of the 2011 Tenth International Symposium on Autonomous Decentralized Systems. :139–146. Abstract

Dynamic environments may include autonomous and decentralised components that pose many challenges from the point of view of interoperability, thus triggering research studies in several directions. One recent research direction explores the automatic composition of heterogeneous systems through connectors synthesised at run-time. Besides functional properties, such connectors generally need to satisfy also non-functional (dependability-related) properties. This paper investigates the definition of an automated procedure to support the synthesis of dependable connectors.

Bertolino A, Calabro A, Giandomenico FD, Martinucci M, Masci P.  2011.  Automated Refinement of Dependability Analysis through Monitoring in Dynamically Connected Systems. Proceedings of the 2011 Tenth International Symposium on Autonomous Decentralized Systems. :315–318. Abstract

Model-based analysis is a well-established method to assess the dependability of a system before deployment. It is well known that, in highly dynamic contexts, the accuracy of the analysis results can be limited because unpredictable phenomena may affect the system during its operation. In such contexts, the analysis typically needs to be refined with data obtained from real system executions. In this paper we tackle the issue of refining model-based dependability analysis in automated systems through monitoring. Specifically, we report on our preliminary results on the development of a system that exploits the synergic use of an automated approach for model-based dependability analysis and a flexible monitoring architecture.

Masci P, Curzon P, Huang H, Ruksenas R, Blandford A, Furniss D, Rajkomar A.  2011.  Towards a formal framework for reasoning about the resilience of dynamic interactive systems. Proceedings of the 13th European Workshop on Dependable Computing. :109–110. Abstract

It is well known that systems built with resilient components are not necessarily resilient systems. Nevertheless, when studying the resilience of work systems characterised by continuous inter-operations among humans and devices, analysts generally concentrate only on localised interactions among humans and devices. Consequently they fail to capture the distributed nature of the mechanisms that guide interactions in dynamic interactive systems. In this paper, as a result of work on the resilience of medical systems with respect to human error, we propose a framework for reasoning about the resilience of complex dynamic interactive systems. To do this we exploit concepts from three different areas: the automated synthesis of resilient systems, formal methods for user-centred design, and distributed cognition.

Masci P, Curzon P.  2011.  Checking User-Centred Design Principles in Distributed Cognition Models: A Case Study in the Healthcare Domain. Information Quality in e-Health. 7058:95-108. Abstract

We propose a constructive procedure for building a distribut-ed cognition model of a system out of contextual / ethnographic data. We then show how such a model can be conveniently used for studying, in a repeatable and justifiable way, if a system correctly implements selected user-centred design principles. Our approach thus complements user studies in that it enables reasoning about the situated use of a teamwork system even before direct user involvement. We have applied our procedure to a healthcare case study. In particular, we have re-analysed a well-known adverse incident that led to a fatality and for which a comprehensive investigation report is in the public domain. By reasoning about the distributed cognition model, we identified several issues that were not addressed in the incident report nor in other subsequent analyses.

Masci P, Nostro N, Giandomenico F.  2011.  On Enabling Dependability Assurance in Heterogeneous Networks through Automated Model-Based Analysis. Software Engineering for Resilient Systems. 6968:78-92. Abstract

We present the specification of a basic library of dependability mechanisms that can be used within automated approaches for synthesising dependable connectors in heterogeneous networks. The library builds on classical dependability patterns, such as majority voting and retry, and uses the concept of overlay networks for triggering the synthesis of specific dependability mechanisms in the connector from high-level specifications. We translated such dependability mechanisms into SAN models with the aim to evaluate, through model-based analysis, which dependability mechanisms should be embedded in the synthesised connector for ensuring a given dependability level between networked systems willing to be connected. A case study is also presented to show the application of selected library mechanisms. This work is carried out in the context of connect, a European FET project which is investigating the possibility of enabling long-lasting inter-operation among networked systems by synthesising mediating connectors at run-time.

Bernardeschi C, Cassano L, Domenici A, Masci P.  2010.  Debugging PVS Specifications of Control Logics via Event-driven Simulation. Proc. 1st Intl. Conf. on Computational Logics, Algebras, Programming, Tools, and Benchmarking (ComputationTools2010). Abstract

In this paper, we present a framework aimed at simulating control logics specified in the higher-order logic of the Prototype Verification System. The framework offers a library of predefined modules, a method for the composition of more complex modules, and an event-driven simulation engine. A developer simulates the specified system by providing its input waveforms as functions from time to logic levels. Once the simulation experiments give sufficient confidence in the correctness of the specification, the model can serve as a basis for the formal verification of desired properties of interest. A simple case study from a nuclear power plant application is shown. This paper is a contribution to research aimed at improving the development process of safety-critical systems by integrating simulation and formal specification methods.

Giandomenico FD, Kwiatkowska M, Martinucci M, Masci P, Qu H.  2010.  Dependability analysis and verification for CONNECTed systems. Proceedings of the 4th international conference on Leveraging applications of formal methods, verification, and validation - Volume Part II. :263–277. Abstract

The Connect project aims to enable the seamless composition of heterogeneous networked systems. In this context, Verification and Validation (V&V) techniques are sought to ensure that the Connected system satisfies dependability requirements. Stochastic model checking and state-based stochastic methods are two appealing V&V approaches to accomplish this task. In this paper, we report on the application of the two approaches in a typical Connect scenario. Specifically, we make clear (i) how the two approaches can be employed to enhance the confidence in the correctness of the analysis, and (ii) how the complementarity of these approaches can be fruitfully exploited to extend the analysis.

Masci P, Chiaradonna S, Giandomenico FD.  2010.  Dependability Analysis of Diffusion Protocols in Wireless Networks with Heterogeneous Node Capabilities. Proceedings of the 2010 European Dependable Computing Conference. :145–154. Abstract

Wireless networks are starting to be populated by interconnected devices that reveal remarkable hardware and software differences. This fact raises a number of questions on the applicability of available results on dependability-related aspects of communication protocols, since they were obtained for wireless networks with homogeneous nodes. In this work, we study the impact of heterogeneous communication and computation capabilities of nodes on dependability aspects of diffusion protocols for wireless networks. We build a detailed stochastic model of the logic layers of the communication stack with the SAN formalism. The model takes into account relevant real-world aspects of wireless communication, such as transitional regions and capture effect, and heterogeneous node capabilities. Dependability-related metrics are evaluated with analytical solutions techniques for small networks, while simulation is employed in the case of large networks.

Bertolino A, Di Giandomenico F, Marco DA, Issarny V, Martinelli F, Masci P, Matteucci I, Saadi R, Sabetta A.  2010.  Dependability in dynamic, evolving and heterogeneous systems: the Connect approach. Proc. 2nd International Workshop on Software Engineering for Resilient Systems (SERENE2010). Abstract

The EU Future and Emerging Technologies (FET) Project CONNECT aims at dropping the heterogeneity barriers that prevent the eternality of networking systems through a revolutionary approach: to synthesise on-the-fly the CONNECTors via which networked systems communicate. The CONNECT approach, however, comes at risk from the standpoint of dependability, stressing the need for methods and tools that ensure resilience to faults, errors and malicious attacks of the dynamically CONNECTed system. We are investigating a comprehensive approach, which combines dependability analysis, security enforcement and trust assessment, and is centred around a lightweight adaptive monitoring framework. In this project paper, we overview the research that we are undertaking towards this objective and propose a unifying workflow process that encompasses all the CONNECT dependability/security/trust concepts and models.

Bertolino A, Di Giandomenico F, Marco DA, Masci P, Sabetta A.  2010.  Metrics for QoS analysis in dynamic, evolving and heterogeneous connected systems. Proc 8th International Workshop on Dynamic Analysis (WODA2010). :–. Abstract

Dynamic, evolving systems pose new challenges from the point of view of Quality of Service (QoS) analysis, calling for techniques able to combine traditional offline methods with new ones applied at run-time. Tracking the evolution and updating the assessment consistently with such system evolution require not only advanced analysis methods, but also appropriate metrics well representative of QoS properties in the addressed context. The ongoing European project Connect addresses systems evolution, and aims at bridging technological gaps arising from heterogeneity of networked systems, by synthesising on-the-fly interoperability connectors. Moving from such ambitious goal, in this paper we present a metrics framework, whereby classical dependability/QoS metrics can be refined and combined to characterise Connect applications and to support their monitoring and analysis.

Avvenuti M, Bernardeschi C, Francesco ND, Masci P.  2009.  A tool for checking secure interaction in Java Cards. Proceedings of the 12th European Workshop on Dependable Computing, EWDC 2009 12th European Workshop on Dependable Computing, EWDC 2009. :8pages. Abstract

We present an approach based on a multilevel security policy and the theory of abstract interpretation for checking secure interaction between applications in Java Cards. The security policy is defined by the user, which assigns security levels to Java Card applications. Actual values are abstracted into security levels, and an abstract interpreter executes the bytecode of applications in the abstract domain. We show JCSI, a tool that implements the presented approach. JCSI can be used to check the binary code of Java Card.

Bernardeschi C, Masci P, Pfeifer H.  2009.  Analysis of Wireless Sensor Network Protocols in Dynamic Scenarios. SSS09, the 11th International Symposium on Stabilization, Safety, and Security of Distributed Systems. 5873:105–119. Abstract

We describe an approach to the analysis of protocols for wireless sensor networks in scenarios with mobile nodes and dynamic link quality. The approach is based on the theorem proving system PVS and can be used for formal specification, automated simulation and verification of the behaviour of the protocol. In order to demonstrate the applicability of the approach, we analyse the reverse path forwarding algorithm, which is the basic technique used for diffusion protocols for wireless sensor networks.

Masci P, Tedeschi A.  2009.  Modelling and Evaluation of a Game-Theory Approach for Airborne Conflict Resolution in Omnet++. 2nd International Conference on Dependability (DEPEND09). :162–165. Abstract

Airborne self-separation is an air-traffic management concept in which pilots are allowed to select the optimal route for the aircraft in real time. In such environments, pilots are assisted by an airborne system that detects possible route conflicts with neighbouring aircraft and gives advice for maneuvering solutions to avoid conflicts. In this paper, we evaluate a game-theory approach for conflict resolutions between aircraft.We modelled the aircraft in a well established simulation framework. Preliminary results give an insight into the dependability of the approach when dealing with the lossy nature of the wireless environment.

Bernardeschi C, Masci P, Pfeifer H.  2008.  Early Prototyping of Wireless Sensor Network Algorithms in PVS. SAFECOMP. :346–359. Abstract

We describe an approach of using the evaluation mechanism of the specification and verification system PVS to support formal design exploration of WSN algorithms at the early stages of their development. The specification of the algorithm is expressed with an extensible set of programming primitives, and properties of interest are evaluated with ad hoc network simulators automatically generated from the formal specification. In particular, we build on the PVSio package as the core base for the network simulator. According to requirements, properties of interest can be simulated at different levels of abstraction. We illustrate our approach by specifying and simulating a standard routing algorithm for wireless sensor networks.