The field of Human-Centred Explainable AI (HCXAI) has been rapidly expanding. In turn, there has been an increase in the number of papers suggesting design principles for HCXAI. However, it is unclear the extent to which design requirements overlap between papers, and in turn what the field overall considers to be HCXAI design requirements. To overcome this, this study analysed the state of the field via a scoping review of papers suggesting HCXAI design requirements, and a Content Analysis of the extracted principles. A total of 330 design principles were identified from 35 papers, which were subsequently categorised into 43 codes and grouped into 4 main areas of focus. Based on these findings, we propose a definition of HCXAI which identifies HCXAI as a design process rather than an XAI technique. Finally, an overview of the current state of HCXAI is presented, as well as areas where further research is required.

Existing classification frameworks for AI and autonomous systems are being outpaced by recent advancements in AI technologies. This limits their applicability to modern intelligent systems, particularly agentic AI systems (autonomous systems that leverage foundation models to achieve wide-ranging, multi-layered goals). To address this deficiency, we introduce INSYTE, a multi-faceted framework that supports the classification of AI systems ranging from traditional rule-based systems to cutting-edge embodied AI and agentic systems. To that end, INSYTE considers the essential characteristics of an AI system across eight key dimensions grouped into four categories: system design ( underspecification and adaptiveness ); functionality ( breadth and depth ); operating environment ( diversity and dynamism ); and independence from human operational control ( intervention and oversight ). Different AI systems (or versions of systems) yield different ‘patterns’ on an eight-axis radar chart that INSYTE uses to provide an immediate visual summary of an AI system’s overall capability and a detailed representation of its individual characteristics. The INSYTE framework aligns with OECD’s definition of deployed AI systems, which is becoming the standard definition used by legislators and developers worldwide.

In the standard interaction model of clinical decision support systems, the system makes a recommendation, and the clinician decides whether to act on it. However, this model can compromise the patient-centeredness of care and the level of clinician involvement. There is scope to develop alternative interaction models, but we need methods for exploring and comparing these to assess how they may impact clinical decision-making. Through collaborating with clinical, AI safety, and HCI experts, and patient representatives, we co-designed a number of alternative human-AI interaction models for clinical decision-making. We then translated these models into ‘Wizard of Oz’ prototypes, where we created clinical scenarios and designed user interfaces with different types of AI output. In this paper, we present alternative models of human-AI interaction and illustrate how we used a co-design approach to translate them into functional prototypes that can be tested with users to explore potential impacts on clinical decision-making.

Assurance cases are used to communicate and assess confidence in critical system properties such as safety and security. Historically, assurance cases have been manually created documents, which are evaluated by system stakeholders through lengthy and complicated processes. In recent years, model-based system assurance approaches have gained popularity to improve the efficiency and quality of system assurance activities. This becomes increasingly important, as systems becomes more complex, it is a challenge to manage their development life-cycles, including coordination of development, verification and validation activities, and change impact analysis in inter-connected system assurance artifacts. Moreover, there is a need for assurance cases that support evolution during the operational life of the system, to enable continuous assurance in the face of an uncertain environment, as Robotics and Autonomous Systems (RAS) are adopted into society. In this paper, we contribute ACCESS - Assurance Case Centric Engineering of Safety-critical Systems, an engineering methodology, together with its tool support, for the development of safety critical systems around evolving model-based assurance cases. We show how model-based system assurance cases can trace to heterogeneous engineering artifacts (e.g. system architectural models, system safety analysis, system behaviour models, etc.), and how formal methods can be integrated during the development process. We demonstrate how assurance cases can be automatically evaluated both at development and runtime. We apply our approach to a case study based on an Autonomous Underwater Vehicle (AUV).

RoboChart is a graphical language for model-based engineering of robotic systems, in the style of UML and SysML. It contains notations for data structures, system architecture, and the behaviour of individual robotic controllers using state machines. Crucially, RoboChart has a formal semantics in the CSP process algebra, which provides a precise foundation for software engineering and formal verification using model checking. However, due to state explosion, the application of model checking does not scale. In this paper, we contribute a compositional verification technique that uses Isabelle/HOL RoboChart state machines symbolically. Our technique uses state invariants to capture safety requirements over a very large or infinite state, similar to the B method, and is highly automated using Isabelle’s sledgehammer tool. We give a model transformation from the RoboTool development environment to Isabelle/HOL and apply this to several verification case studies.

Assurance cases (ACs) are an established practice for arguing confidence in critical system properties such as safety and security in high-risk industries.ACs use system artifacts to argue the aforementioned properties.Due to the iterative nature of system development, we need to update ACs to maintain assurance validity as a system evolves.For example, a changed design or an added hazard would result in re-evaluation of claims or a new claim to be verified.Thus, the generation and maintenance of ACs is a labour-intensive process.With the growing application of Model-based Engineering (MBE) in system development, it is beneficial to generate ACs from design models because this captures traceability, and enables automatic AC creation and update driven by model modification.Accordingly, the contribution of this paper is an automatic approach to AC generation and assembly from both unstructured design artifacts and UML-like design models within Eclipse.This approach also supports AC evidence generation by formal verification facilitated by automatically generated assertions.The realization of AC assembly and verification is supported by model query and model transformation.We apply our approach to an autonomous underwater robot with the RoboChart robotics modelling language.

General-purpose I/O widely exists on multi- and many-core systems. For real-time applications, I/O operations are often required to be timing-predictable, i.e., bounded in the worst case, and timing-accurate, i.e., occur at (or near) an exact desired time instant. Unfortunately, both timing requirements of I/O operations are hard to achieve from the system level, especially for many-core architectures, due to various latency and contention factors presented in the path of instigating an I/O request. This paper considers a dedicated I/O co-processing unit, and proposes two scheduling methods, with the necessary hardware support implemented. It is the first work that guarantees timing predictability and maximises timing accuracy of I/O tasks in the multi-and many-core systems.

Ecological Momentary Assessment (EMA) tools are used to monitor the thoughts and feelings of people in their everyday lives over time. In this paper we examine the feasibility of multi-item, multi-subject Hidden Markov Models (HMMs) to identify response clusters in people with schizophrenia. Data comprise 49 participants from two randomised clinical trials using the mobile app ClinTouch, an EMA tool for daily monitoring of schizophrenia symptoms. The app was used for up to 12 weeks (median follow-up 83 days, 78% response rate). We find that a 3-cluster model with 3 states per cluster performs best amongst the configurations tested, and the feasibility of HMMs as applied to multi-item EMA data is demonstrated. However, there is substantial heterogeneity between participants within each hidden state for which sampling error due to short observation periods is a likely contributor. More data are needed to validate and refine the modelling approach taken here.

Abstract Safety‐critical systems are of paramount importance for many application domains, where safety properties are a key driver to engineer critical aspects and avoid system failures. For the benefits of large‐scale reuse, software product lines (SPL) have been adopted in critical systems industry. However, the integration of safety analysis in the SPL development process is nontrivial. Also, the different usage contexts of safety‐critical systems complicates component fault modeling tasks and the identification of potential hazards. In this light, better methods become necessary to estimate the impact of dependability properties during Hazard Analysis and Risk Assessment. Existing methods incorporating the analysis of safety properties in SPL are limited as they do not include hazard analysis and component fault modeling. In this paper, we present the novel DEPendable Software Product Line Engineering (DEPendable‐SPLE) approach, which extends traditional SPL processes to support the reuse of safety assets. We also present a detailed analysis of the impact of product and context features on the SPL design, safety analysis, and safety requirements. We applied DEPendable‐SPLE to a realistic case study from the aerospace domain to illustrate how to model and reuse safety properties. DEPendable‐SPLE reduced the effort of safety analysis for certifying system variants.

Software systems are increasingly expected to cope with variable workloads, component failures and other uncertainties through self-adaptation. As such, self-adaptive software has been the subject of intense research over the past decade [3, 4, 9, 10].

For software quality assurance, many safety-critical industries appeal to the use of dynamic testing and structural coverage criteria. However, there are reasons to doubt the adequacy of such practices. Mutation testing has been suggested as an alternative or complementary approach but its cost has traditionally hindered its adoption by industry, and there are limited studies applying it to real safety-critical code. This paper evaluates the effectiveness of state-of-the-art mutation testing on safety-critical code from within the U.K. nuclear industry, in terms of revealing flaws in test suites that already meet the structural coverage criteria recommended by relevant safety standards. It also assesses the practical feasibility of implementing such mutation testing in a real setting. We applied a conventional selective mutation approach to a C codebase supplied by a nuclear industry partner and measured the mutation score achieved by the existing test suite. We repeated the experiment using trivial compiler equivalence (TCE) to assess the benefit that it might provide. Using a conventional approach, it first appeared that the existing test suite only killed 82% of the mutants, but applying TCE revealed that it killed 92%. The difference was due to equivalent or duplicate mutants that TCE eliminated. We then added new tests to kill all the surviving mutants, increasing the test suite size by 18% in the process. In conclusion, mutation testing can potentially improve fault detection compared to structural-coverage-guided testing, and may be affordable in a nuclear industry context. The industry feedback on our results was positive, although further evidence is needed from application of mutation testing to software with known real faults.

Building on concepts drawn from control theory, self-adaptive software handles environmental and internal uncertainties by dynamically adjusting its architecture and parameters in response to events such as workload changes and component failures. Self-adaptive software is increasingly expected to meet strict functional and non-functional requirements in applications from areas as diverse as manufacturing, healthcare and finance. To address this need, we introduce a methodology for the systematic ENgineering of TRUstworthy Self-adaptive sofTware (ENTRUST). ENTRUST uses a combination of (1) design-time and runtime modelling and verification, and (2) industry-adopted assurance processes to develop trustworthy self-adaptive software and assurance cases arguing the suitability of the software for its intended application. To evaluate the effectiveness of our methodology, we present a tool-supported instance of ENTRUST and its use to develop proof-of-concept self-adaptive software for embedded and service-based systems from the oceanic monitoring and e-finance domains, respectively. The experimental results show that ENTRUST can be used to engineer self-adaptive software systems in different application domains and to generate dynamic assurance cases for these systems.

We describe dynamic safety cases, a novel operationalization of the concept of through-life safety assurance, whose goal is to enable proactive safety management. Using an example from the aviation systems domain, we motivate our approach, its underlying principles, and a lifecycle. We then identify the key elements required to move towards a formalization of the associated framework.

Software plays a key role in high-risk systems, i.e., safety and security-critical systems. Several certification standards and guidelines, e.g., in the defense, transportation (aviation, automotive, rail), and healthcare domains, now recommend and/or mandate the development of assurance cases for software-intensive systems. As such, there is a need to understand and evaluate (a) the application of assurance cases to software, and (b) the relationship between the development and assessment of assurance cases, and software engineering concepts, processes and techniques. The ICSE 2013 Workshop on Assurance Cases for Software-intensive Systems (ASSURE) aims to provide an international forum for high-quality contributions (research, practice, and position papers) on the application of assurance case principles and techniques for software assurance, and on the treatment of assurance cases as artifacts to which the full range of software engineering techniques can be applied.

Testing provides a primary means for assuring software in safety-critical systems. To demonstrate, particularly to a certification authority, that sufficient testing has been performed, it is necessary to achieve the test coverage levels recommended or mandated by safety standards and industry guidelines. Mutation testing provides an alternative or complementary method of measuring test sufficiency, but has not been widely adopted in the safety-critical industry. In this study, we provide an empirical evaluation of the application of mutation testing to airborne software systems which have already satisfied the coverage requirements for certification. Specifically, we apply mutation testing to safety-critical software developed using high-integrity subsets of C and Ada, identify the most effective mutant types, and analyze the root causes of failures in test cases. Our findings show how mutation testing could be effective where traditional structural coverage analysis and manual peer review have failed. They also show that several testing issues have origins beyond the test activity, and this suggests improvements to the requirements definition and coding process. Our study also examines the relationship between program characteristics and mutation survival and considers how program size can provide a means for targeting test areas most likely to have dormant faults. Industry feedback is also provided, particularly on how mutation testing can be integrated into a typical verification life cycle of airborne software.

We describe our experience with the ongoing development of a safety case for an unmanned aircraft system (UAS), emphasizing autopilot software safety assurance. Our approach combines formal and non-formal reasoning, yielding a semi-automatically assembled safety case, in which part of the argument for autopilot software safety is automatically generated from formal methods. This paper provides a discussion of our experiences pertaining to (a) the methodology for creating and structuring safety arguments containing heterogeneous reasoning and information (b) the comprehensibility of, and the confidence in, the arguments created, and (c) the implications of development and safety assurance processes. The considerations for assuring aviation software safety, when using an approach such as the one in this paper, are also discussed in the context of the relevant standards and existing (process-based) certification guidelines.

Safety cases capture a structured argument linking claims about the safety of a system to the evidence justifying those claims. However, arguments in safety cases tend to be predominantly qualitative. Partly, this is attributed to the lack of sufficient design and operational data necessary to measure the achievement of high-dependability goals, particularly for safety-critical functions implemented in software. The subjective nature of many forms of evidence, such as expert judgment and process maturity, also contributes to the overwhelming dependence on qualitative arguments. However, where data for quantitative measurements can be systematically collected, quantitative arguments provide benefits over qualitative arguments in assessing confidence in the safety case. In this paper, we propose a basis for developing and evaluating the confidence in integrated qualitative and quantitative safety arguments. We specify a safety argument using the Goal Structuring Notation (GSN), identify and quantify uncertainties therein, and use Bayesian Networks (BNs) as a means to reason about confidence in a probabilistic way. We illustrate our approach using a fragment of a safety case for an unmanned aircraft system (UAS).

The process can fail to deliver its expected outputs and consequently contribute to the introduction of faults into the software system. The process may fail due to ambiguous and unsuitable notations, unreliable tool-support, flawed methods and techniques or incompetent personnel. However, not all process activities pose the same degree of risks and therefore require the same degree of rigour. In this paper, we define an extendable metamodel for describing lifecycle processes. The metamodel embodies attributes which facilitate the automated analysis of the process, revealing possible process failures and associated risks. The metamodel also provides the capability to automatically verify the compliance of the process with certification standards. The metamodel is evaluated against processes from the aerospace and automotive domains.

The introduction of a software product line may pose a great organizational challenge in the domain of highintegrity systems. Project and technical managers within an organization need to be assured that the reusable assets of a product line are reliable and trustworthy, particularly when project teams do not have full control over the development of these assets. In this paper we report on our experience with the establishment of a software product line for an aerospace Engine Monitoring Unit (EMU). Specifically, we report on challenges encountered with the configuration management and certification of EMU products derived from the product line. These two areas are still to be addressed adequately by the product line community as they are central for the management of product line assets across different projects within an organization.