Cookies Policy
We use cookies to improve our site and your experience. By continuing to browse our site you accept our cookie policy. Find out More
Close
  • Menu
Interest
Topics
Details

Details

  • Name

    Michael Douglas Harrison
  • Cluster

    Computer Science
  • Role

    External Research Collaborator
  • Since

    01st March 2015
Publications

2017

The Specification and Analysis of Use Properties of a Nuclear Control System

Authors
Harrison, MD; Masci, PM; Campos, JC; Curzon, P;

Publication
The Handbook of Formal Methods in Human-Computer Interaction.

Abstract

2016

Evaluation of Formal IDEs for Human-Machine Interface Design and Analysis: The Case of CIRCUS and PVSio-web

Authors
Fayollas, Camille; Martinie, Celia; Palanque, PhilippeA.; Masci, Paolo; Harrison, MichaelD.; Campos, JoseCreissac; Silva, SauloRodriguese;

Publication
Proceedings of the Third Workshop on Formal Integrated Development Environment.

Abstract
Critical human-machine interfaces are present in many systems including avionics systems and medical devices. Use error is a concern in these systems both in terms of hardware panels and input devices, and the software that drives the interfaces. Guaranteeing safe usability, in terms of buttons, knobs and displays is now a key element in the overall safety of the system. New integrated development environments (IDEs) based on formal methods technologies have been developed by the research community to support the design and analysis of high-confidence human-machine interfaces. To date, little work has focused on the comparison of these particular types of formal IDEs. This paper compares and evaluates two state-of-the-art toolkits: CIRCUS, a model-based development and analysis tool based on Petri net extensions, and PVSio-web, a prototyping toolkit based on the PVS theorem proving system.

2016

Formal Verification of a Space System's User Interface With the IVY Workbench

Authors
Campos, JC; Sousa, M; Bergue Alves, MCB; Harrison, MD;

Publication
IEEE TRANSACTIONS ON HUMAN-MACHINE SYSTEMS

Abstract
This paper describes the application of the IVY workbench to the formal analysis of a user interface for a safety-critical aerospace system. The operation manual of the system was used as a requirement document, and this made it possible to build a reference model of the user interface, focusing on navigation between displays, the information provided by each display, and how they are interrelated. Usability-related property specification patterns were then used to derive relevant properties for verification. This paper discusses both the modeling strategy and the analytical results found using the IVY workbench. The purpose of the reference model is to provide a standard against which future versions of the interface may be assessed.

2016

Templates as heuristics for proving properties of medical devices

Authors
Harrison, MD; Campos, JC; Masci, P; Curzon, P;

Publication
EAI Endorsed Trans. Creative Technologies

Abstract
This paper briefly describes how property templates have been used to analyse and explore the interactive behaviour of a specific medical device (an IV infusion pump). It is proposed that interactive devices that satisfy properties based on the templates are easier and safer to use. The property templates act as heuristics for the development of suitable properties tailored to the details of the particular device. A mathematically based approach is used to prove that a specification of the device satisfies the properties. Copyright © 2015 ICST.

2016

Modelling information resources and their salience in medical device design

Authors
Harrison, MD; Campos, JC; Ruksenas, R; Curzon, P;

Publication
Proceedings of the 8th ACM SIGCHI Symposium on Engineering Interactive Computing Systems, EICS 2016, Brussels, Belgium, June 21-24, 2016

Abstract
The paper describes a model that includes an explicit description of the information resources that are assumed to guide use, enabling a focus on properties of "plausible interactions". The information resources supported by an interactive system should be designed to encourage the correct use of the system. These resources signpost a user's interaction, helping to achieve desired goals. Analysing assumptions about information resource support is particularly relevant when a system is safety critical that is when interaction failure consequences could be dangerous, or walk-up-and-use where interaction failure may lead to reluctance to use with expensive consequences. The paper shows that expressing these resource constraints still provides a wider set of behaviours than would occur in practice. A resource may be more or less salient at a particular stage of the interaction and as a result potentially overlooked. For example, the resource may be accessible but not used because it does not seem relevant to the current goal. The paper describes how the resource framework can be augmented with additional information about the salience of the assumed resources. A medical device that is in common use in many hospitals is used as illustration. c 2016 ACM.