This paper presents a multimodal human-robot interaction (HRI) system for educational contexts implemented on the humanoid robot Pepper. The system leverages multiple communicative channels, allowing learners to combine speech with tablet interaction while the robot responds through synchronized speech, textual captions and dynamic visual cues. To ensure robustness and reliability, we introduce the use of Metamorphic Testing for multimodal HRI. By validating system behavior through systematic input transformations, we demonstrate how metamorphic testing can uncover inconsistencies across linguistic, visual and cross-modal interactions. This work contributes both a novel methodological framework for evaluating multimodal HRI systems and an application to educational robotics.

Falsification, whose aim is to detect unsafe behaviors of cyber-physical systems (CPS) that violate signal temporal logic (STL) specifications, has been actively investigated in the past decade. Although numerous falsification approaches have been proposed, the falsification community suffers from a shortage of benchmarks that hinders a thorough assessment of those falsification approaches. In this article, we bridge this gap by proposing an automated approach for generating falsification benchmarks. Our approach is data-driven: first, we generate different time-variant traces (acting as system output traces) that satisfy a given STL specification, and we associate these with corresponding system input traces; then, we use these input and output traces to train an LSTM model that generalizes them. These models can serve as benchmarks for assessing falsification approaches against the given specification. In the experimental evaluation, we validate the generated models by measuring their ability to differentiate the performance of different falsification approaches. Our generated models expose strengths and weaknesses of all the considered falsification approaches, which was not achieved by benchmarks currently used in the falsification community. These results demonstrate the usefulness of our approach and can potentially push forward subsequent research in falsification.

Cyber-physical systems (CPSs) are increasingly adopting deep neural networks (DNNs) as controllers, giving birth to AI-enabled CPSs . Despite their advantages, many concerns arise about the safety of DNN controllers. Numerous efforts have been made to detect system executions that violate safety specifications; however, once a violation is detected, to fix the issue, it is necessary to localise the parameters of the DNN controller responsible for the wrong decisions leading to the violation. This is particularly challenging, as it requires to consider a sequence of control decisions, rather than a single one, preceding the violation. To tackle this problem, we propose SpectAcle , that can localise the faulty parameters in DNN controllers. SpectAcle considers the DNN inferences preceding the specification violation and uses forward impact to determine the DNN parameters that are more relevant to the DNN outputs. Then, it identifies which of these parameters are responsible for the specification violation, by adapting classic suspiciousness metrics. Moreover, we propose two versions of SpectAcle , that consider differently the timestamps that precede the specification violation. We experimentally evaluate the effectiveness of SpectAcle on 6,067 faulty benchmarks, spanning over different application domains. The results show that SpectAcle can detect most of the faults.

In AI-enabled CPSs, DNNs are used as controllers for the physical system. Despite their advantages, DNN controllers can produce wrong control decisions, which can lead to safety risks for the system. Once wrong behaviors are detected, the DNN controller should be fixed. DNN repair is a technique that allows to perform this fine-grained improvement. However, state-of-the-art DNN repair techniques require ground-truth labels to guide the repair. For AI-enabled CPSs, these are not available, as it is not possible to assess whether a specific control decision is correct. Nevertheless, it is possible to assess whether the DNN controller leads to wrong behaviors of the controlled system by considering system-level requirements. In this paper, following this observation, we propose a novel DNN repair approach that is guided by system-level specifications. The approach takes in input a system-level specification, some tests violating the specification, and some faulty DNN weights. The approach searches for alternative weight values with the goal of fixing the behavior on the failing tests without breaking the passing tests. We also propose a heuristic that allows us to accelerate the search by avoiding the execution of some tests. Experiments on real-world AI-enabled CPSs show that the approach effectively repairs their controllers.

Modern Cyber-Physical Systems (CPSs) that need to perform complex control tasks (e.g., autonomous driving) are increasingly using AI-enabled controllers, mainly based on deep neural networks (DNNs). The quality assurance of such types of systems is of vital importance. However, their verification can be extremely challenging, due to their complexity and uninterpretable decision logic. Falsification is an established approach for CPS quality assurance, which, instead of attempting to prove the system correctness, aims at finding a time-variant input signal violating a formal specification describing the desired behavior; it often employs a search-based testing approach that tries to minimize therobustnessof the specification, given by its quantitative semantics. However, guidance provided by robustness is mostly black-box and only related to the system output, but does not allow to understand whether the temporal internal behavior determined by multiple consecutive executions of the neural network controller has been explored sufficiently. To bridge this gap, in this paper, we make an early attempt at exploring the temporal behavior determined by the repeated executions of the neural network controllers in hybrid control systems and first propose eight time-aware coverage criteria specifically designed for neural network controllers in the context of CPS, which consider different features by design: the simple temporal activation of a neuron, the continuous activation of a neuron for a given duration, and the differential neuron activation behavior over time. Second, we introduce a falsification framework, named$\mathtt {FalsifAI}$, that exploits the coverage information for better falsification guidance. Namely, inputs of the controller that increase the coverage (so improving theexplorationof the DNN behaviors), are prioritized in theexploitationphase of robustness minimization. Our large-scale evaluation over a total of 3 typical CPS tasks, 6 system specifications, 18 DNN models and more than 12,000 experiment runs, demonstrates 1) the advantage of our proposed technique in outperforming two state-of-the-art falsification approaches, and 2) the usefulness of our proposed time-aware coverage criteria for effective falsification guidance.

Abstract Hybrid system falsification is an important quality assurance method for cyber-physical systems with the advantage of scalability and feasibility in practice than exhaustive verification. Falsification, given a desired temporal specification, tries to find an input of violation instead of a proof guarantee. The state-of-the-art falsification approaches often employ stochastic hill-climbing optimization that minimizes the degree of satisfaction of the temporal specification, given by its quantitativerobust semantics. However, it has been shown that the performance of falsification could be severely affected by the so-calledscale problem, related to the different scales of the signals used in the specification (e.g., rpm and speed): in the robustness computation, the contribution of a signal could bemaskedby another one. In this paper, we propose a novel approach to tackle this problem. We first introduce a new robustness definition, calledQB-Robustness, which combines classical Boolean satisfaction and quantitative robustness. We prove that QB-Robustness can be used to judge the satisfaction of the specification and avoid the scale problem in its computation. QB-Robustness is exploited by a falsification approach based on Monte Carlo Tree Search over the structure of the formal specification. First, tree traversal identifies the sub-formulas for which it is needed to compute the quantitative robustness. Then, on the leaves, numerical hill-climbing optimization is performed, aiming to falsify such sub-formulas. Our in-depth evaluation on multiple benchmarks demonstrates that our approach achieves better falsification results than the state-of-the-art falsification approaches guided by the classical quantitative robustness, and it is largely not affected by the scale problem.