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.

Abstract
Formal methods technologies have the potential to verify the usability and safety of user interface (UI) software design in medical devices, enabling significant reductions in use errors and consequential safety incidents with such devices. This however depends on comprehensive and verifiable safety requirements to leverage these techniques for detecting and preventing flaws in UI software that can induce use errors. This paper presents a hazard analysis method that extends Leveson’s System Theoretic Process Analysis (STPA) with a comprehensive set of causal factor categories, so as to provide developers with clear guidelines for systematic identification of use-related hazards associated with medical devices, their causes embedded in UI software design, and safety requirements for mitigating such hazards. The method is evaluated with a case study on the Gantry-2 radiation therapy system, which demonstrates that (1) as compared to standard STPA, our method allowed us to identify more UI software design issues likely to cause use-related hazards; and (2) the identified UI software design issues facilitated the definition of precise, verifiable safety requirements for UI software, which could be readily formalized in verification tools such as Prototype Verification System (PVS).

Abstract
One way of contributing to a demonstration that a medical device is acceptably safe is to show that the device satisfies a set of requirements known to mitigate hazards. This paper describes experience using formal techniques to model an IV infusion device and to prove that the modelled device captures a set of requirements. The requirements chosen for the study are based on a draft proposal developed by the US Food and Drug Administration (FDA). A major contributor to device related errors are (user) interaction errors. For this reason the chosen models and requirements focus on user interface related issues.

Abstract
The Proceedings of the ACM (PACM) was initiated by ACM in 2015 as overarching framework for publishing high quality computer science research. The goal for these new journals is to provide an alternate journal publication model for rigorous research papers that have traditionally been presented at major ACM conferences. PACM titles cross multiple intellectual communities, and each separate PACM is designed to represent a broad, but consistent, reach area. This is the first issue of the Proceedings of the ACM on Human Computer Interaction (PACMHCI), which represents the varied topics and communities that compose the broader study of Human Computer Interaction (HCI). The rich heterogeneity of this field can be expressed as deep ethnographies of information use in context, to experiments showing the effectiveness of interface designs, to the production of new technologies that push the limits of how we interact with computers, and much more. The production of PACMHCI will focus on content associated with major research communities that are supported by the ACM Special Interest Group on Human-Computer Interaction (SIGCHI). Individual issues will be largely associated with separate research communities, who may then also select papers from the issue for presentation at their major conferences. These research communities provide the volunteers and editors necessary to provide the rigorous review and editorial process that will define this journal. Those editors will serve on the overall board for ACMHCI, to help bridge our diverse communities. Leveraging our research communities allows us to provide high-quality reviewing while maintaining the quick processing of work that is important in this quickly moving field. This inaugural issue of PACMHCI represents work from the Engineering Interactive Computing Systems (EICS) community. 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 research community is to create novel and high quality contributions in this direction. Although there are only three articles in this first issue, our pipeline for future issues is promising. In the first submission cycle, 41 papers were submitted and, of those, 22 were asked for major revisions. We expect a good number of those 22 papers to be ultimately accepted over the coming months. We are grateful to our newly-formed Editorial Board consisting of more than 70 experts for lending their support and knowledge to the new journal. More information about PACMHCI can be found at http://pacmhci.acm.org/.

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
This chapter explores a layered approach to the analysis of the Nuclear Power Plant Control System described in Chap. 4. A model is specified to allow the analysis of use-centred properties based on generic templates. User interface properties include the visibility of state attributes, the clarity of the mode structure and the ease with which an action can be recovered from. Property templates are used as heuristics to ease the construction of requirements for the control system interface.