2017
Authors
Harrison, MD; Masci, P; Campos, JC; Curzon, P;
Publication
IEEE TRANSACTIONS ON HUMAN-MACHINE SYSTEMS
Abstract
One part of demonstrating that a device is acceptably safe, often required by regulatory standards, is to show that it satisfies a set of requirements known to mitigate hazards. This paper is concerned with how to demonstrate that a user interface software design is compliant with use-related safety requirements. A methodology is presented based on the use of formal methods technologies to provide guidance to developers about addressing three key verification challenges: 1) how to validate a model, and show that it is a faithful representation of the device; 2) how to formalize requirements given in natural language, and demonstrate the benefits of the formalization process; and 3) how to prove requirements of a model using readily available formal verification tools. A model of a commercial device is used throughout the paper to demonstrate the methodology. A representative set of requirements are considered. They are based on US Food and Drug Administration (FDA) draft documentation for programmable medical devices, and on best practice in user interface design illustrated in relevant international standards. The methodology aims to demonstrate how to achieve the FDA's agenda of using formal methods to support the approval process for medical devices.
2014
Authors
Silva, JL; Campos, JC; Harrison, MD;
Publication
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.
2015
Authors
Almeida, D; Campos, JC; Saraiva, J; Silva, JC;
Publication
30TH ANNUAL ACM SYMPOSIUM ON APPLIED COMPUTING, VOLS I AND II
Abstract
This paper presents a catalog of smells in the context of interactive applications. These so-called usability smells are indicators of poor design on an application's user interface, with the potential to hinder not only its usability but also its maintenance and evolution. To eliminate such usability smells we discuss a set of program/usability refactorings. In order to validate the presented usability smells catalog, and the associated refactorings, we present a preliminary empirical study with software developers in the context of a real open source hospital management application. Moreover, a tool that computes graphical user interface behavior models, giving the applications' source code, is used to automatically detect usability smells at the model level.
2017
Authors
Harrison, MD; Masci, PM; Campos, JC; Curzon, P;
Publication
The Handbook of Formal Methods in Human-Computer Interaction.
Abstract
2017
Authors
Harrison, MD; Drinnan, M; Campos, JC; Masci, P; Freitas, L; di Maria, C; Whitaker, M;
Publication
FORMAL ASPECTS OF COMPONENT SOFTWARE (FACS 2017)
Abstract
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.
2015
Authors
Campos, JC; Abade, T; Silva, JL; Harrison, MD;
Publication
AMBIENT ASSISTED LIVING: ICT-BASED SOLUTIONS IN REAL LIFE SITUATIONS
Abstract
APEX, a framework for prototyping ubiquitous environments, is used to design an Ambient Assisted Living (AAL) system to enhance a care home for older people. The environment allows participants in the design process to experience the proposed design and enables developers to explore the design by rapidly developing alternatives. APEX provided the means to explore alternative designs through a virtual environment. It provides a mediating representation (a boundary object) allowing users to be involved in the design process. A group of residents in a city-based care home were involved in the design. The paper describes the design process and lessons learnt for the design of AAL systems.
The access to the final selection minute is only available to applicants.
Please check the confirmation e-mail of your application to obtain the access code.