Cookies
Usamos cookies para melhorar nosso site e a sua experiência. Ao continuar a navegar no site, você aceita a nossa política de cookies. Ver mais
Aceitar Rejeitar
  • Menu
Publicações

Publicações por Michael Douglas Harrison

2016

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

Autores
Fayollas, C; Martinie, C; Palanque, P; Masci, P; Harrison, MD; Campos, JC; Silva, SRE;

Publicação
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

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

Publicação
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.

2014

Rapid development of first person serious games using the APEX platform: The Asthma Game

Autores
Gomes, T; Abade, T; Campos, JC; Harrison, M; Silva, JL;

Publicação
Proceedings of the ACM Symposium on Applied Computing

Abstract
Serious games combine a ludic component with instructive and formative goals. They aim to educate and train through play. This paper explores the use of a development framework for dynamic virtual environments to develop serious games. The framework (APEX) was originally developed to prototype ubiquitous computing environments. Here it is used to develop a first person serious game: the Asthma Game. This game aims to teach children with asthma how to act to prevent attacks by drawing attention to asthma triggers in the home, and by providing information about how to avoid them. Besides the description of the game, results about the viability and utility of the approach are also discussed.

2013

Automated theorem proving for the systematic analysis of an infusion pump

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

Publicação
ECEASST

Abstract

2014

Analysing interactive devices based on information resource constraints

Autores
Campos, JC; Doherty, G; Harrison, MD;

Publicação
INTERNATIONAL JOURNAL OF HUMAN-COMPUTER STUDIES

Abstract
Analysis of the usability of an interactive system requires both an understanding of how the system is to be used and a means of assessing the system against that understanding. Such analytic assessments are particularly important in safety-critical systems as latent vulnerabilities may exist which have negative consequences only in certain circumstances. Many existing approaches to assessment use tasks or scenarios to provide explicit representation of their understanding of use. These normative user behaviours have the advantage that they clarify assumptions about how the system will be used but have the disadvantage that they may exclude many plausible deviations from these norms. Assessments of how a design fails to support these user behaviours can be a matter of judgement based on individual experience rather than evidence. We present a systematic formal method for analysing interactive systems that is based on constraints rather than prescribed behaviour. These constraints capture precise assumptions about what information resources are used to perform action. These resources may either reside in the system itself or be external to the system. The approach is applied to two different medical device designs, comparing two infusion pumps currently in common use in hospitals. Comparison of the two devices is based on these resource assumptions to assess consistency of interaction within the design of each device.

2014

Prototyping and analysing ubiquitous computing environments using multiple layers

Autores
Silva, JL; Campos, JC; Harrison, MD;

Publicação
INTERNATIONAL JOURNAL OF HUMAN-COMPUTER STUDIES

Abstract
If ubiquitous computing (ubicomp) is to enhance physical environments then early and accurate assessment of alternative solutions will be necessary to avoid costly deployment of systems that fail to meet requirements. This paper presents APEX, a prototyping framework that combines a 3D Application Server with a behaviour modeling tool. The contribution of this framework is that it allows exhaustive analysis of the behaviour models that drive the prototype while at the same time enabling immersive exploration of a virtual environment simulating the proposed system. The development of prototypes is supported through three layers: a simulation layer (using OpenSimulator); a modelling layer (using CPN Tools) and a physical layer (using external devices and real users). APEX allows movement between these layers to analyse different features, from user experience to user behaviour. The multi layer approach makes it possible to express user behaviour in the modelling layer, provides a way to reduce the number of real users needed by adding simulated avatars, and supports user testing of hybrids of virtual and real components as well as exhaustive analysis. This paper demonstrates the approach by means of an example, placing particular emphasis on the simulation of virtual environments, low cost prototyping and the formal analysis capabilities.

  • 1
  • 3