Abstract
[Extract] It is our great pleasure to welcome you to the first issue of PACMHCI EICS, which features full papers appearing at the 9th ACM SIGCHI Symposium on Engineering Interactive Systems (EICS’17). The conference takes place in Lisbon, Portugal on 26-29 June, 2017. EICS gathers researchers that aim to improve the ways we build interactive systems. Building interactive systems is a multi-faceted and challenging activity, involving a plethora of different actors and roles. This is particularly true in the domain of HCI, where we continuously push the edge of what is possible, where there is a crucial need for adequate processes, tools and methods to build reliable, useful and usable systems that help people cope with the ever-increasing complexity of work and life. The primary goal of the EICS conference series is to provide a venue for novel and high quality contributions in this direction...

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.

Abstract

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.

Abstract
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.

Abstract
An approach to design Ambient Assisted Living systems is presented, which is based on APEX, a framework for prototyping ubiquitous environments. The approach is illustrated through the design of a smart environment within a care home for older people. Prototypes allow participants in the design process to experience the proposed design and enable developers to explore design alternatives rapidly. APEX provides the means to explore alternative environment designs virtually. The prototypes developed with APEX offered a mediating representation, 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 as well as lessons learned for the future design of AAL systems.