As IoT devices age they must be replaced to maintain reliability and performance. During upgrades, ensuring interoperability among new and existing devices is critical for preserving designated system behaviours. Existing formal verification approaches rely on system documentation or source code to build formal models or extract flat models from system logs. We propose a novel log-driven verification framework that automatically discovers executable Hierarchical Colored Petri Nets (HCPNs) from raw IoT system logs. The framework integrates model checking to verify cross-layer interoperability during IoT system evolution and device replacement. We demonstrate the effectiveness of our approach using a street lighting system study.

Advances in digital fabrication with flexible and conductive materials are enabling new opportunities for customisable wearables that enhance physical training across various sports through on-body posture and movement monitoring.However, before developing new wearable devices, it is crucial to understand the unique challenges and opportunities of real-world use and the diverse needs of stakeholders such as athletes, trainers, and sports enthusiasts.In this paper, we report results of two co-design workshops conducted with 11 participants representing a range of sports backgrounds and interests to identify challenges and opportunities for flexible wearables.The participants' designs and prototypes highlight the importance of supporting personalised wearable design, addressing varying contexts, and accommodating different skill levels.We propose design considerations for wearable devices that prioritise flexibility, both in their materiality to support a wide range of movement and in their adaptability to accommodate changing conditions and user progression across skill levels.

Designing positive robot experiences requires an understanding of users' perceptions and meeting their needs in an ethical manner. However, despite best intentions, users have strong positive or negative reactions to robots, either finding them “cute“ or “creepy”. The Perceived Creepiness of Technology Scale (PCTS) was designed for evaluating how creepy a technology appears to a user on first encounter. In this paper we applied the PCTS to a cross-section of social robots to measure their perceived creepiness and evaluate the strengths and weaknesses of PCTS when applied in a Human-Robot Interaction (HRI) context. We demonstrate that while a robot may not be perceived as creepy initially, it can have underlying unethical practices inherent in its design which is not well captured by the PCTS. This emphasises the need for better HRI practices to ensure creepiness is appropriately assessed in the social robot domain.

The use of robust software engineering processes is essential in the design and development of interactive systems. This ensures that software is both functionally correct and also usable in the required context. There are a variety of software engineering techniques that can be used to consider different aspects of a system under construction, and at different stages in the development process. There is, however, a natural tension between formal approaches (typically used in the domain of safety-critical systems to consider functional correctness) and informal design approaches, which focus on users and user requirements in a manner which is accessible by stakeholders. In this paper we present two new approaches which enable a tighter coupling of informal design requirements with formal models. We present examples of these two approaches and discuss the benefits that transformations between the informal and formal provide. We also discuss the current limitations of such work along with recommendations about how these might be addressed.

The rapid growth in the number of Internet of Things (IoT) systems and their increasing use in safety-critical domains has led to the need for an evolution of development methods. Model-Driven Development (MDD) approaches have been used in software engineering to reduce development time and minimise errors in implemented systems. This paper introduces a novel Model-Driven Development (MDD) approach for Internet of Things (IoT) systems which considers interactivity from the perspective of both users and IoT components. A real-world example is presented to explain the motivation for the work and demonstrate the benefits and use of lightweight interactive system models adapted for the design and development of IoT systems.

Abstract Within the software engineering community, deciding how to collect, store and use personal data has become about more than just understanding our users. This paper considers ethical data use that includes cultural considerations and data ownership rights. We discuss indigenous data sovereignty as a concept and how it potentially impacts technological solutions that gather personal data from users. We propose an extension to typical user-centred design processes, which we call participatory data design. This incorporates the use of frameworks and tools that specifically focus on managing data within the cultural context it is gathered from. We also present a specific example of how we have used this approach in the context of a data collection project from Māori workers in New Zealand forestry. We conclude with a discussion of the wider implications of this approach.

Informal design artefacts allow end-users and non-experts to contribute to software design ideas and development. In contrast, software engineering techniques such as model-driven development support experts in ensuring quality properties of the software they propose and build. Each of these approaches have benefits which contribute to the development of robust, reliable and usable software, however it is not always obvious how best to combine these two. In this paper we describe a novel technique which allows us to use informal design artefacts, in the form of ideation card designs, to generate formal models of IoT applications. To implement this technique, we created the Cards-to-Model (C2M) tool which allows us to automate the model generation process. We demonstrate this technique with a case study for a safety-critical IoT application called “Medication Reminders”. By generating formal models directly from the design we reduce the complexity of the modelling process. In addition, by incorporating easy-to-use informal design artefacts in the process we allow non-experts to engage in the design and modelling process of IoT applications.

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 Task models are used in many different ways throughout the design and development of interactive systems. When the interactive systems are safety critical, task models can play an important role in ensuring system behaviours are consistent with user requirements, which may help to prevent errors. While task models can be used to describe a user’s goals and the steps required to achieve that goal, to understand where user errors may occur we also need to consider the users’ understanding of how to perform a task and how this relates to the system they are using. Our focus is on the use of medical devices such as syringe drivers and infusion pumps for intravenous medication, which forms a major part of hospital inpatient care throughout the world. While we might rely on software engineering and human factors techniques to ensure correctness of such devices, their use by medical personnel in practice includes other factors that are equally important. These include training medical personnel in the use of medical devices. Also numeracy education for medical staff to ensure that they are able to set up and perform the necessary calculations to convert prescribed medication into the appropriate values and measures for their delivery mechanisms. We have developed an approach that aims to bring together concepts of technology design (both functional correctness and usability concerns), numeracy and medication delivery competency. In order to do so we use task models as a common language that enables us to consider these different domains in a single way. We find that the ability to describe the two domains within a single process allows us to compare models of knowledge, tasks and use of devices, which can elicit potential mismatches and problems.

Task models have been used for decades in interactive system design and there are several mature modelling approaches with corresponding tool support. However, in our own work, we have also experienced their limitations, especially in situations where task models are partial ancillary models and not primary artifacts. This was one of the motivations for this paper, which presents a systematic examination of literature to better understand the current place of task models in the continual evolution of user-centred software development practices. While overview work in this domain typically focuses on the analysis of representative task modelling notations and/or tools and relies on foundation papers, we apply a mixed top-down and bottom-up approach to identify relevant themes and trends in the use of task models over the last twenty-years. The paper identifies and discusses dominant patterns of use as well as gaps. It provides a comprehensive framing of both past and present trends in task modelling and supports those who want to incorporate task modelling in their own work. From this we identify areas of research that should receive greater attention in order to address future considerations.

The area of Engineering Interactive Computing Systems (EICS) is defined as the intersection between Software Engineering (SE) and Human-Computer Interaction (HCI). In this paper, we provide an overview of what EICS is and how it is positioned with respect to other venues in HCI, such as CHI, UIST, and IUI, highlighting its legacy and paying homage to past scientific events from which EICS emerged. We also take this opportunity to deliver a comparative analysis of the past, present, and perhaps future research and development questions raised in EICS by analyzing the EICS papers published from its first edition to this one, based on global and chronological word clouds, phrase nets, and topic modelling.

Testing is an important part of the software engineering process to help ensure that systems will behave as expected. In this paper we investigate interactive system testing, taking into consideration the different components of the system. Interactive systems have three different components, the interactive, functional and overlap. The interactive component is the interface of the interactive system, the functional the underlying instructions of the interactive system, and the overlap component the point at which the interactive and functional components intersect. The interactive and functional components are often tested separately, however, problems can occur where these components overlap. Therefore, in this paper we present a model-based testing approach specifically designed to inspect the overlap component behaviour and to ensure that it behaves as expected.

To gain confidence in safety-critical interactive systems, formal modelling and analysis plays a vital role. The aim of this paper is to use Coloured Petri Nets to model and analyze safety-critical interactive systems. We present a technique to construct a single Coloured Petri Net model of the user interface, interaction and functionality of safety-critical interactive systems and then analyze the achieved Coloured Petri Net model using a state space analysis method. There are several reasons for using Coloured Petri Nets. Coloured Petri Nets provides a graphical representation and hierarchical structuring mechanism, and a state space verification technique, which allows querying the state space to investigate behaviours of a system. There are several tools that supports Coloured Petri Nets including the CPN Tool which helps in building CPN models and allows simulation and analysis using state spaces. The technique to model and analyze safety-critical interactive systems is illustrated using a simplified infusion pump example.

Within the domain of interactive system development and design, particularly for safety-critical systems, there is an inherent tension between formalisms used for software engineering methodologies and the creative aspects of design. In this paper we consider how we might better unify these by way of a framework for design spaces and design artefacts. We present formal definitions for simple and complex design spaces and then describe how they are incorporated into traces. We then discuss how these can be used to reason about considerations such as preservation of requirements and iterative changes throughout the design process and provide some small examples of this.

Model-based development of interactive systems provides a number of benefits which can support the creation of robust and correct systems, particularly important when the interactive systems are safety-critical. Many different approaches have been proposed which target the models at different aspects of the development process (for example task analysis, interface layouts, functional behaviours etc.) and which can be used in different ways (verification of correctness, plasticity, usability). One of the aims for any modelling method should be simplicity - we are after all trying to hide complexity via abstraction in order to make reasoning about systems more tractable than working at the programming level. One of the challenges that exists however we do our modelling is ensuring the consistency between the model of the interface and interactivity and model of the functional behaviour of the system. This is primarily due to the different types of models that most naturally describe these different elements. In this paper we propose a method of tightening the integration of models of these different components of the system by generating obligations which explicitly describe the coupling of functional behaviour with interactive elements. We then show how these obligations can be used to support the development process during the programming and testing of the system.

Abstract Formal approaches to software development require that we correctly describe (or specify) systems in order to prove properties about our proposed solution prior to building it. We must then follow a rigorous process to transform our specification into an implementation to ensure that the properties we have proved are retained. Different transformation, or refinement, methods exist for different formal methods, but they all seek to ensure that we can guide the transformation in a way which preserves the desired properties of the system. Refinement methods also allow us to subsequently compare two systems to see if a refinement relation exists between the two. When we design and build the user interfaces of our systems we are similarly keen to ensure that they have certain properties before we build them. For example, do they satisfy the requirements of the user? Are they designed with known good design principles and usability considerations in mind? Are they correct in terms of the overall system specification? However, when we come to implement our interface designs we do not have a defined process to follow which ensures that we maintain these properties as we transform the design into code. Instead, we rely on our judgement and belief that we are doing the right thing and subsequent user testing to ensure that our final solution remains useable and satisfactory. We suggest an alternative approach, which is to define a refinement process for user interfaces which will allow us to maintain the same rigorous standards we apply to the rest of the system when we implement our user interface designs.