Similarity is a key property across two or more interactive systems. Indeed, interacting with similar systems can bring benefits (e.g., reduced learning efforts and training time) but may also raise issues (e.g., interference errors and higher cognitive load). Interactive systems may be similar, as they correspond to the same work and tasks performed with different underlying systems, such as the pilots’ tasks in the cockpit of an Airbus A320 and a Boeing 737. They may also be similar by design, as they belong to the same suite as, for instance, the Microsoft Office software suite, where several tools are designed to be used concurrently by the same users. Previous work on similarity has focused on the visual presentation of interactive applications, highlighting commonalities and differences in terms of layout, shape, colours and other features of the user interface. This paper proposes a systematic and formal approach to analyse and assess the similarity between several interactive systems, focusing on their behaviours. To this end, we propose a tool-supported process that exploits both interactive formal system behaviour models and user task models. These models are analysed with the help of formal tools (model checking) to identify commonalities and differences in their exhibited behaviours. Beyond, we compare the specific and generic behavioural properties of each model, which provide semantic and meaningful information about how similar they are and how they differ. The approach is applied to two similar critical command and control interactive systems for flight safety operations in the space domain.

A generation of interoperable devices is emerging in control systems. Devices can be controlled by users at multiple levels. The devices that are controlled may be certified as safe by their vendors, but new issues may arise from their integration and remote use, as new interaction pathways will be enabled that are simply not possible when the device is used as a stand-alone system. This paper is concerned with modelling concrete interfaces that are designed to enable use of these systems. It builds on previous work concerned with proving use-centred safety properties across the interoperable system. The concern of this paper however is describing the relationship between an abstract model and a concrete interface that reflects more concretely the tasks that the users are intended to perform. In the example used in this paper, a menu interface is built on top of the abstract interface. The primary concern of the paper is describing the relationship between the abstract interface and the specified concrete interface. Properties of the interface that were discussed in previous work are proved of the concrete interface. This paper uses, as an example, use-centred safety properties of integrated clinical environments for remote medical care. Four properties are considered briefly: consistency , completeness , feedback and reversibility with an understanding of the tasks that users may perform. More detail will be given to the first two with a particular focus on the relation between the abstract interaction model and a concrete menu based model. The properties are formalised in the language of the PVS verification system. They are mechanically verified using the PVS proof assistant for a model of a realistic prototype of an integrated clinical environment. The presented analysis is intended to be performed during system design and development, and before the actual system is deployed, to increase confidence that the design complies with important use-centred safety properties that capture design guidelines discussed in usability engineering standards. It is envisaged that such an analysis could help inform a safety assessment of the integrated system.

Models - at different levels of abstraction and pertaining to different engineering views - are central in the design of railway networks, in particular signalling systems. The design of such systems must follow numerous strict rules, which may vary from project to project and require information from different views. This renders manual verification of railway networks costly and error-prone.

Abstract This editorial introduces the special issue of Interacting with Computer on Heterogeneous Models and Modelling Approaches for Engineering of Interactive Systems. This special issue was proposed to gather the best contributions from a series of workshops organized alongside conferences such as FM’19 (3rd World Congress on Formal Methods) and EICS’19 (11th ACM SIGCHI Symposium on Engineering Interactive Computing Systems). It also encompasses papers submitted directly to this special issue.

Abstract This paper explores the role of formal methods as part of the user-centred design of interactive systems. An iterative process is described, developing prototypes incrementally, proving user-centred requirements while at the same time evaluating the prototypes that are executable forms of the developed models using ‘traditional’ techniques for user evaluation. A formal analysis complements user evaluations. This approach enriches user-centred design that typically focuses understanding on context and producing sketch designs. These sketches are often non-functional (e.g. paper) prototypes. They provide a means of exploring candidate design possibilities using techniques such as cooperative evaluation. This paper describes a further step in the process using formal analysis techniques. The use of formal methods provides a systematic approach to checking plausibility and consistency during early design stages, while at the same time enabling the generation of executable prototypes. The technique is illustrated through an example based on a pill dispenser.

Use error due to user interface design defects is a major concern in many safety critical domains, for example avionics and health care. Early detection of latent user interface problems can be facilitated by user-centered design methods that integrate formal verification technologies. This article considers the role that formal verification technologies can play in the context of user-centered design by considering the following three existing tools: CIRCUS, PVSio-web, and IVY. These tools have been developed to support the model based analysis of critical user interfaces. They have their foundations in existing formal verification technologies, but each of them is focused towards particular issues relating to user interface design. The article explores the different phases of the user-centered design process and the extent to which each of these tools supports these phases. Criteria are developed for assessing their role at each stage of the design process. The results of the evaluation provide guidance to developers to help choose the most appropriate tool based on their analysis needs while at the same time setting challenges for future developments.

The paper describes templates for model-based analysis of usability and safety aspects of user interface software design. The templates crystallize general usability principles commonly addressed in user-centred safety requirements, such as the ability to undo user actions, the visibility of operational modes, and the predictability of user interface behavior. These requirements have standard forms across different application domains, and can be instantiated as properties of specific devices. The modeling and analysis process is carried out using the Prototype Verification System (PVS), and is further facilitated by structuring the specification of the device using a format that is designed to be generic across interactive systems. A concrete case study based on a commercial infusion pump is used to illustrate the approach. A detailed presentation of the automated verification process using PVS shows how failed proof attempts provide precise information about problematic user interface software features.

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

Ensuring that an interactive application allows users to perform their activities and reach their goals is critical to the overall usability of the interactive application. Indeed, the effectiveness factor of usability directly refers to this capability. Assessing effectiveness is a real challenge for usability testing as usability tests only cover a very limited number of tasks and activities. This paper proposes an approach towards automated testing of effectiveness of interactive applications. To this end we resort to two main elements: an exhaustive description of users' activities and goals using task models, and the generation of scenarios (from the task models) to be tested over the application. However, the number of scenarios can be very high (beyond the computing capabilities of machines) and we might end up testing multiple similar scenarios. In order to overcome these problems, we propose strategies based on task models manipulations (e.g., manipulating task nodes, operator nodes, information...) resulting in a more intelligent test case generation approach. For each strategy, we investigate its relevance (both in terms of test case generation and in terms of validity compared to the original task models) and we illustrate it with a small example. Finally, the proposed strategies are applied on a real-size case study demonstrating their relevance and validity to test interactive applications.

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

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.

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.

The ever increasing number of platforms and languages available to software developers means that the software industry is reaching high levels of complexity. Model Driven Architecture (MDA) presents a solution to the problem of improving software development processes in this changing and complex environment. MDA driven development is based on models definition and transformation. Design patterns provide a means to reuse proven solutions during development. Identifying design patterns in the models of a MDA approach helps their understanding, but also the identification of good practices during analysis. However, when analyzing or maintaining code that has not been developed according to MDA principles, or that has been changed independently from the models, the need arises to reverse engineer the models from the code prior to patterns' identification. The approach presented herein consists in transforming source code into models, and infer design patterns from these models. Erich Gamma's cataloged patterns provide us a starting point for the pattern inference process. MapIt, the tool which implements these functionalities is described.

Abstract. Formal approaches to the design of interactive systems rely on reasoning about properties of the system at a very high level of abstraction. Specifications to support such an approach typically provide little scope for reasoning about presentations and the representation of information in the presentation. In contrast, psychological theories such as distributed cognition place a strong emphasis on the role of representations, and their perception by the user, in the cognitive process. However, the post-hoc techniques for the observation and analysis of existing systems which have developed out of the theory do not help us in addressing such issues at the design stage. Mn this paper we show how a formalisation can be used to investigate the representational aspects of an interface. Our goal is to provide a framework to help identify and resolve potential problems with the representation of information, and to support understanding of representational issues in design. We present a model for linking properties at the abstract and perceptual levels, and illustrate its use in a case study of a ight deck instrument. There is a widespread consensus that proper tool support is a prerequisite for the adoption of formal techniques, but the use of such tools can have a profound effect on the process itself. In order to explore this issue, we apply a higher-order logic theorem prover to the analysis.