Abstract
Formal verification can be a complementary approach to UCD, offering a systematic and repeatable process to address the demands of designing safety and mission-critical interactive systems. However, the practical application of formal verification often encounters barriers to accessibility for non-technical stakeholders. In the case of model checking, although the verification step is fully automated, developing the required specifications and interpreting the verification results requires considerable technical expertise in formal methods. Recent developments in generative Artificial Intelligence (AI) have driven proposals for Large Language Models (LLMs) to be applied throughout various phases of software engineering. This begs the question of whether LLMs might be used to help bridge the gap between formal techniques and tools and stakeholders lacking technical expertise. This paper explores how these questions might be addressed in the context of an ongoing effort aimed at translating model-checking counter-examples into natural language explanations, making them accessible to designers and domain experts.

Abstract
The growing integration of Artificial Intelligence (AI) into interactive systems presents unique challenges and opportunities for Human-Computer Interaction (HCI) and User Experience (UX). While AI can enhance usability and provide novel interaction paradigms, it also raises concerns related to transparency, control, and user trust. This workshop seeks to bring together researchers and practitioners to discuss state-of-the-art engineering methods that support HCI and UX in AI-driven systems. By fostering interdisciplinary collaboration, we aim to identify key challenges, share best practices, and develop a roadmap for future research in this critical area.

Abstract
Safety-critical interactive systems pose design and evaluation challenges that go beyond usability. The safety of the system (i.e. the guarantee that it does not reach an undesirable or incorrect state) is also a relevant consideration. Traditional user-centred approaches (UCD) lack the rigour and thoroughness needed to address safety, and formal verification arises as a possible solution. Applying formal verification to a safety-critical interactive system design encompasses developing a model, expressing and verifying properties, and analysing the verification results. In the case of model checking, properties are typically expressed in temporal logic. This creates a gap between the languages used in UCD and the languages used for formal verification. Creating temporal logic properties manually requires expertise in formal methods and can be both time-consuming and error-prone. This paper explores how a patterns-based approach can be used to support the specification of properties in a natural language-based style. A prototype implementation of the approach is evaluated through a user study, and the results of this evaluation are discussed.

Abstract
This workshop proposal is the third edition of a workshop which has been organised at EICS 2023 and EICS 2024. This edition aims to bring together researchers and practitioners interested in the engineering of interactive systems that embed AI technologies (as for instance, AI-based recommender systems) or that use AI during the engineering lifecycle. The overall objective is to identify (from experience reported by participants) methods, techniques, and tools to support the use and inclusion of AI technologies throughout the engineering lifecycle for interactive systems. A specific focus is on guaranteeing that user-relevant properties such as usability and user experience are accounted for. Contributions are also expected to address system-related properties, including resilience, dependability, reliability, or performance. Another focus is on the identification and definition of software architectures supporting this integration.

Abstract

Abstract