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. CEUR Workshop Proceedings, vol 727 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 (EWDC11). :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.