Abstract Trust is a multi-faceted phenomenon traditionally studied in human relations and more recently in human-machine interactions. In the context of AI-enabled systems, trust is about the belief of the user that in a given scenario the system is going to be helpful and safe. The system-side counterpart to trust is trustworthiness. When trust and trustworthiness are aligned with each other, there is calibrated trust. Trust, trustworthiness, and calibrated trust are all dynamic phenomena, evolving throughout the history and evolution of user beliefs, systems, and their interaction. In this paper, we review the basic concepts of trust, trustworthiness and calibrated trust and provide definitions for them. We discuss their various metrics used in the literature, and the causes that may affect their dynamics, particularly in the context of AI-enabled systems. We discuss the implications of the discussed concepts for various types of stakeholders and suggest some challenges for future research.

Abstract With the emergence of autonomous vehicles comes the requirement of adequate and rigorous testing, particularly in critical scenarios that are both challenging and potentially hazardous. Generating synthetic simulation-based critical scenarios for testing autonomous vehicles has therefore received considerable interest, yet it is unclear how such scenarios relate to the actual crash or near-crash scenarios in the real world. Consequently, their realism is unknown. In this paper, we define realism as the degree of similarity of synthetic critical scenarios to real-world critical scenarios. We propose a methodology to measure realism using two metrics, namely attribute distribution and Euclidean distance. The methodology extracts various attributes from synthetic and realistic critical scenario datasets and performs a set of statistical tests to compare their distributions and distances. As a proof of concept for our methodology, we compare synthetic collision scenarios from DeepScenario against realistic autonomous vehicle collisions collected by the Department of Motor Vehicles in California, to analyse how well DeepScenario synthetic collision scenarios are aligned with real autonomous vehicle collisions recorded in California. We focus on five key attributes that are extractable from both datasets, and analyse the attribution distribution and distance between scenarios in the two datasets. Further, we derive recommendations to improve the realism of synthetic scenarios based on our analysis. Our study of realism provides a framework that can be replicated and extended for other dataset both concerning real-world and synthetically-generated scenarios.

The practice of testing software systems modelled as Finite State Machines (FSMs) has garnered significant attention owing to its simplicity. In FSM-based testing, the tester derives a test suite from the FSM model representing the system’s specification. Subsequently, this test suite is executed against the implementation, and the tester uses the output to decide whether the implementation conforms to the specification. Often, a test suite generation technique requires input sequences to check whether the FSM is in the intended state. This task is referred to asstate identificationand is often carried out using a set of input sequences called a characterising set. Even though the use of characterising sets simplifies testing, they require a reliable reset or reset sequence and additional transfer sequences. Unfortunately, resetting the underlying system can be costly or may entail manual configuration. In addition, transfer sequences do not directly contribute to testing. This work introduces a class of characterising sets (Ordered Characterising Sets(O-WSets)) that avoid using resets or transfers by design. We show that checking the existence of such a characterising set is NP-complete. We introduce the notion of bounded O-WSets (BO-WSets), which are types of O-WSets that limit transfer usage, and give an algorithm that constructs these. In experiments, on average, the proposed approach led to reductions in the number of resets (95% for real FSMs; 99.73% for synthetic FSMs), the number of transfer inputs (53% for real FSMs; 63.3% for synthetic FSMs) and the number of inputs in state identification sequences (50% for real FSMs; 66.6% for synthetic FSMs). Additionally, the proposed algorithm reduced the time and memory required to derive state identification sequences by 85% and 23%, respectively. Finally, the approach led to test suites with 49.3% fewer sequences and 33.3% fewer inputs on average.

Automatic generation of random test inputs is an approach that can alleviate the challenges of manual test case design. However, random test cases may be ineffective in fault detection and increase testing cost, especially in systems where test execution is resource- and time-consuming. To remedy this, the domain knowledge of test engineers can be exploited to select potentially effective test cases. To this end, test selection constraints suggested by domain experts can be utilized either for filtering randomly generated test inputs or for direct generation of inputs using constraint solvers. In this article, we propose a domain specific language (DSL) for formalizing locality-based test selection constraints of autonomous agents and discuss the impact of test selection filters, specified in our DSL, on randomly generated test cases. We study and compare the performance of filtering and constraint solving approaches in generating selective test cases for different test scenario parameters and discuss the role of these parameters in test generation performance. Through our study, we provide criteria for suitability of the random data filtering approach versus the constraint solving one under the varying size and complexity of our testing problem. We formulate the corresponding research questions and answer them by designing and conducting experiments using QuickCheck for random test data generation with filtering and Z3 for constraint solving. Our observations and statistical analysis indicate that applying filters can significantly improve test efficiency of randomly generated test cases. Furthermore, we observe that test scenario parameters affect the performance of the filtering and constraint solving approaches differently. In particular, our results indicate that the two approaches have complementary strengths: random generation and filtering works best for large agent numbers and long paths, while its performance degrades in the larger grid sizes and more strict constraints. On the contrary, constraint solving has a robust performance for large grid sizes and strict constraints, while its performance degrades with more agents and long paths.

Testing is a crucial phase in the development of complex systems, and this has led to interest in automated test generation techniques based on state-based models. Many approaches use models that are types of finite state machine (FSM). Corresponding test generation algorithms typically require that certain test components, such as reset sequences (RSs) and preset distinguishing sequences (PDSs), have been produced for the FSM specification. Unfortunately, the generation of RSs and PDSs is computationally expensive, and this affects the scalability of such FSM-based test generation algorithms. This paper addresses this scalability problem by introducing a reinforcement learning framework: the$\mathcal{Q}$-Graph framework for MBT. We show how this framework can be used in the generation of RSs and PDSs and consider both (potentially partial) timed and untimed models. The proposed approach was evaluated using three types of FSMs: randomly generated FSMs, FSMs from a benchmark, and an FSM of an Engine Status Manager for a printer. In experiments, the proposed approach was much faster and used much less memory than the state-of-the-art methods in computing PDSs and RSs.

Abstract Active automata learning has been a successful technique to learn the behaviour of state-based systems by interacting with them through queries. In this paper, we develop a compositional algorithm for active automata learning in which systems comprising interleaving parallel components are learned compositionally. Our algorithm automatically learns the structure of systems while learning the behaviour of the components. We prove that our approach is sound and that it learns a maximal set of interleaving parallel components. We empirically evaluate the effectiveness of our approach and show that our approach requires significantly fewer numbers of input symbols and resets while learning systems. Our empirical evaluation is based on a large number of subject systems obtained from a case study in the automotive domain.

This paper presents an investigation into the effectiveness of introducing explicit causal explanations in a child-robot interaction setting to help children with autism improve their Visual Perspective Taking (VPT) skills. A sample of ten children participated in three sessions with a social robot on different days, during which they played several games consisting of VPT tasks. In some of the sessions, the robot provided constructive feedback to the children by giving causal explanations related to VPT; other sessions were control sessions without explanations. An analysis of the children’s learning progress revealed that they improved their VPT abilities faster when the robot provided causal explanations. However, both groups ultimately reach a similar ratio of correct answers in later sessions. These findings suggest that providing causal explanations using a social robot can be effective to teach VPT to children with autism. This study paves the way for further exploring a robot’s ability to provide causal explanations in other educational scenarios.

We perform a systematic literature review on testing, validation, and verification of robotic and autonomous systems (RAS). The scope of this review covers peer-reviewed research papers proposing, improving, or evaluating testing techniques, processes, or tools that address the system-level qualities of RAS. Our survey is performed based on a rigorous methodology structured in three phases. First, we made use of a set of 26 seed papers (selected by domain experts) and the SERP-TEST taxonomy to design our search query and (domain-specific) taxonomy. Second, we conducted a search in three academic search engines and applied our inclusion and exclusion criteria to the results. Respectively, we made use of related work and domain specialists (50 academics and 15 industry experts) to validate and refine the search query. As a result, we encountered 10,735 studies, out of which 195 were included, reviewed, and coded. Our objective is to answer four research questions, pertaining to (1) the type of models, (2) measures for system performance and testing adequacy, (3) tools and their availability, and (4) evidence of applicability, particularly in industrial contexts. We analyse the results of our coding to identify strengths and gaps in the domain and present recommendations to researchers and practitioners. Our findings show that variants of temporal logics are most widely used for modelling requirements and properties, while variants of state-machines and transition systems are used widely for modelling system behaviour. Other common models concern epistemic logics for specifying requirements and belief-desire-intention models for specifying system behaviour. Apart from time and epistemics, other aspects captured in models concern probabilities (e.g., for modelling uncertainty) and continuous trajectories (e.g., for modelling vehicle dynamics and kinematics). Many papers lack any rigorous measure of efficiency, effectiveness, or adequacy for their proposed techniques, processes, or tools. Among those that provide a measure of efficiency, effectiveness, or adequacy, the majority use domain-agnostic generic measures such as number of failures, size of state-space, or verification time were most used. There is a trend in addressing the research gap in this respect by developing domain-specific notions of performance and adequacy. Defining widely accepted rigorous measures of performance and adequacy for each domain is an identified research gap. In terms of tools, the most widely used tools are well-established model-checkers such as Prism and Uppaal, as well as simulation tools such as Gazebo; Matlab/Simulink is another widely used toolset in this domain. Overall, there is very limited evidence of industrial applicability in the papers published in this domain. There is even a gap considering consolidated benchmarks for various types of autonomous systems.

Abstract We introduce a formal language for specifying dynamic updates for Software Defined Networks. Our language builds upon Network Kleene Algebra with Tests (NetKAT) and adds constructs for synchronisations and multi-packet behaviour to capture the interaction between the control- and data-plane in dynamic updates. We provide a sound and ground-complete axiomatisation of our language. We exploit the equational theory and provide an efficient method for reasoning about safety properties. We implement our equational theory in DyNetiKAT – a tool prototype, based on the Maude Rewriting Logic and the NetKAT tool, and apply it to a case study. We show that we can analyse the case study for networks with hundreds of switches using our tool prototype.

Children with Autism Spectrum Disorder (ASD) often struggle with visual perspective taking (VPT) skills and the understanding that others might have viewpoints and perspectives that are different from their own; i.e., the ability to understand that two or more people looking at the same object from different positions might not see the same thing. The understanding of VPT can be improved by introducing explicit causal explanations in the interactions involving autistic children. Moreover, the use of social robots can help autistic children improve their social skills. We present a retrospective study with Kaspar, a humanoid social robot specifically designed to interact with children with ASD, which aims to define the initial protocol for a study on the effect of causal explanation in VPT provided by Kaspar. To this end, we investigate in which scenarios causal explanations, provided either by researchers or by Kaspar, contribute substantially to the child’s understanding of VPT. The results have helped us identify multiple interaction categories that benefit from causal explanation. We have used these results in order to define new interaction games that benefit from causal explanations. These are now progressing through usability assessment experiments.

We present a novel and generalised notion of doping cleanness for cyber-physical systems that allows for perturbing the inputs and observing the perturbed outputs both in the time- and value-domains. We instantiate our definition using existing notions of conformance for cyber-physical systems. As a formal basis for monitoring conformance-based cleanness, we develop the temporal logic HyperSTL*, an extension of Signal Temporal Logics with trace quantifiers and a freeze operator. We show that our generalised definitions are essential in a data-driven method for doping detection and apply our definitions to a case study concerning diesel emission tests.

Abstract We provide a semantic framework to specify information propagation in social networks; our semantic framework features both the operational description of information propagation and the epistemic aspects in social networks. In our framework, based on annotated labelled transition systems, actions are decorated with function views to specify different types of announcements. Our function views enforce various common types of local privacy policies, i.e. those policies concerning a single action. Furthermore, we specify global privacy policies, those concerning multiple actions, using a combination of modal $\mu $-calculus and epistemic logic. To illustrate the applicability of our framework, we apply it to the specification of a real-world case study. As a fundamental property for the epistemic aspect of our semantic model, we prove that its indistinguishability relations are equivalence relations, namely they are reflexive, symmetric and transitive. We also study the complexity bounds for the model-checking problem concerning a subset of our logic and show that model checking is PSPACE-complete for the studied subset.

Model-based testing is a structured method to test complex systems. Scaling up model-based testing to large systems requires improving the efficiency of various steps involved in testcase generation and more importantly, in test-execution. One of the most costly steps of model-based testing is to bring the system to a known state, best achieved through synchronising sequences. A synchronising sequence is an input sequence that brings a given system to a predetermined state regardless of system’s initial state. Depending on the structure, the system might be complete, i.e., all inputs are applicable at every state of the system. However, some systems are partial and in this case not all inputs are usable at every state. Derivation of synchronising sequences from complete or partial systems is a challenging task. In this paper, we introduce a novel Q-learning algorithm that can derive synchronising sequences from systems with complete or partial structures. The proposed algorithm is faster and can process larger systems than the fastest sequential algorithm that derives synchronising sequences from complete systems. Moreover, the proposed method is also faster and can process larger systems than the most recent massively parallel algorithm that derives synchronising sequences from partial systems. Furthermore, the proposed algorithm generates shorter synchronising sequences.

Abstract We present a novel and generalised notion of doping cleanness for cyber-physical systems that allows for perturbing the inputs and observing the perturbed outputs both in the time– and value–domains. We instantiate our definition using existing notions of conformance for cyber-physical systems. We show that our generalised definitions are essential in a data-driven method for doping detection and apply our definitions to a case study concerning diesel emission tests.

Logical characterisation of a behavioural equivalence relation precisely specifies the set of formulae that are preserved and reflected by the relation. Such characterisations have been studied extensively for exact semantics on discrete models such as bisimulations for labelled transition systems and Kripke structures, but to a much lesser extent for approximate relations, in particular in the context of hybrid systems. We present what is to our knowledge the first characterisation result for approximate notions of hybrid refinement and hybrid conformance involving tolerance thresholds in both time and value. Since the notion of conformance in this setting is approximate, any characterisation will unavoidably involve a notion of relaxation, denoting how the specification formulae should be relaxed in order to hold for the implementation. We also show that an existing relaxation scheme on Metric Temporal Logic used for preservation results in this setting is not tight enough for providing a characterisation of neither hybrid conformance nor refinement. The characterisation result, while interesting in its own right, paves the way to more applied research, as our notion of hybrid conformance underlies a formal model-based technique for the verification of cyber-physical systems.

Cooperative awareness basic services are key components of several Connected Autonomous Vehicles (CAV) functions. We present a rigorous approach to the analysis of cooperative awareness basic services in a CAV setup. Our approach addresses a major challenge in the traditional analysis techniques of such services, namely, coming up with effective scenarios that can meaningfully cover their various behaviours, exercise the limits of these services and come up with a quantitative means for design-space exploration.Our approach integrates model-based testing and search-based testing to automatically generate scenarios and steer the scenario generation process towards generating inputs that can lead to the most severe hazards. Additionally we define other objectives that maximise the coverage of the model and the diversity of the generated test inputs. The result of applying our technique to the analysis of cooperative awareness services leads to automatically generated hazardous scenarios for parameters that abide by the ETSI ITS-G5 vehicular communications standard. We show that our technique can be used as an effective design-space exploration method and can be used to design adaptive protocols that can mitigate the hazards detected through our initial analysis.

Determining and computing root causes in system failures is a significant issue in science and engineering. In this paper, we introduce a notion of causality for explaining counterexamples in system analysis based on formal models. The counter-examples are produced by checking for hazardous situati ons expressed in the Hennessy-Milner Logic, in the context of Labelled Transition System models. We also introduce CauseJMu, a tool for automatically identifying such causal computations within a system model. CauseJMu relies on encoding causality in terms of an extension of Hennessy-Milner Logic to recursive formulae with data. The encodings enable deciding whether a certain computation is causal or not, using the mCRL2 model checker.

Featured Finite State Machines (FFSMs) were proposed as a modeling formalism that represents the abstract behavior of an entire software product line (SPL). Several model-based testing techniques have been developed to support test case generation for SPL specifications, but none support the full fault coverage criterion for SPLs at the family-wide level. In this paper, we propose an extension of the Harmonized State Identifiers (HSI) method, an FSM-based testing method supporting full fault coverage. By extending the HSI method for FFSMs, we are able to generate a single configurable test suite for groups of SPL products that can be instantiated using feature constraints. We implement a graphical tool named ConFTGen to guide the design, validation, derivation and test case generation for state, transition and full fault coverage of FFSMs. Experimental results indicate a reduction of approximately 50% on the number of test cases required to test 20 random SPL products. Also, we investigate the applicability of our method by applying it to a case study from the automotive domain, namely the Body Comfort System.

Regression testing is a means to assure that a change in the software, or its execution environment, does not introduce new defects. It involves the expensive undertaking of rerunning test cases. Several techniques have been proposed to reduce the number of test cases to execute in regression testing, however, there is no research on how to assess industrial relevance and applicability of such techniques. We conducted a systematic literature review with the following two goals: firstly, to enable researchers to design and present regression testing research with a focus on industrial relevance and applicability and secondly, to facilitate the industrial adoption of such research by addressing the attributes of concern from the practitioners’ perspective. Using a reference-based search approach, we identified 1068 papers on regression testing. We then reduced the scope to only include papers with explicit discussions about relevance and applicability (i.e. mainly studies involving industrial stakeholders). Uniquely in this literature review, practitioners were consulted at several steps to increase the likelihood of achieving our aim of identifying factors important for relevance and applicability. We have summarised the results of these consultations and an analysis of the literature in three taxonomies, which capture aspects of industrial-relevance regarding the regression testing techniques. Based on these taxonomies, we mapped 38 papers reporting the evaluation of 26 regression testing techniques in industrial settings.

The analysis of software product lines is challenging due to the potentially large number of products, which grow exponentially in terms of the number of features. Product sampling is a technique used to avoid exhaustive testing, which is often infeasible. In this paper, we propose a classification for product sampling techniques and classify the existing literature accordingly. We distinguish the important characteristics of such approaches based on the information used for sampling, the kind of algorithm, and the achieved coverage criteria. Furthermore, we give an overview on existing tools and evaluations of product sampling techniques. We share our insights on the state-of-the-art of product sampling and discuss potential future work.

Epistemic logic is a powerful formalism for reasoning about communication protocols, particularly in the setting with dishonest agents and lies. Operational frameworks such as algebraic process calculi, on the other hand, are powerful formalisms for specifying the narrations of communication protocols. We bridge these two powerful formalisms by presenting a process calculus in which lies can be told. A lie in our framework is a communicated message that is pretended to be a different message (or nothing at all). In our formalism, we focus on what credulous rational agents can infer about a particular run if they know the protocol beforehand. We express the epistemic properties of such specifications in a rich extension of modal μ-calculus with the belief modality and define the semantics of our operational models in the semantic domain of our logic. We formulate and prove criteria that guarantee belief consistency for credulous agents.

Conformance testing is a formal and structured approach to verifying system correctness. We propose a conformance testing algorithm for cyber-physical systems, based on the notion of hybrid conformance by Abbas and Fainekos. We show how the dynamics of system specification and the sampling rate play an essential role in making sound verdicts. We specify and prove error bounds that lead to sound test-suites for a given specification and a given sampling rate. We use reachability analysis to find such bounds and implement the proposed approach using the CORA toolbox in Matlab. We apply the implemented approach on a case study from the automotive domain.

Conformance testing is a formal and structured approach to verifying system correctness. We propose a conformance testing algorithm for cyber-physical systems, based on the notion of hybrid conformance by Abbas and Fainekos. We show how the dynamics of system specification and the sampling rate play an essential role in making sound verdicts. We specify and prove error bounds that lead to sound test-suites for a given specification and a given sampling rate.

We review and compare three notions of conformance testing for cyber-physical systems. We begin with a review of their underlying semantic models and present conformance-preserving translations between them. We identify the differences in the underlying semantic models and the various design decisions that lead to these substantially different notions of conformance testing. Learning from this exercise, we reflect upon the challenges in designing an "ideal" notion of conformance for cyber-physical systems and sketch a roadmap of future research in this domain.

SystemC is an IEEE standard system-level language used in hardware/software co-design and has been widely adopted in the industry. This paper describes a formal approach to verifying SystemC designs by providing a mapping to the process algebra mCRL2. Our mapping formalizes both the simulation semantics as well as exhaustive state-space exploration of SystemC designs. By exploiting the existing reduction techniques of mCRL2 and also its model-checking tools, we efficiently locate the race conditions in a system and resolve them. A tool is implemented to automatically perform the proposed mapping. This mapping and the implemented tool enabled us to exploit process-algebraic verification techniques to analyze a number of case-studies, including the formal analysis of a single-cycle and a pipelined MIPS processor specified in SystemC.

Module paths are often used to specify the delays of cells in a Verilog cell library description, which define the propagation delay for an event from an input to an output. Specifying such paths manually is an error prone task; a forgotten path is interpreted as a zero delay, which can cause further flaws in the subsequent design steps. Moreover, one can specify superfluous module paths, i.e., module paths that can never occur in any practical run of the model and hence, make excessive restrictions on the subsequent design decision. This paper presents a method to check whether the given module paths are reflected in the functional implementation. Complementing this check, we also present a method to derive module paths from a functional description of a cell.

Synchronous data flow graphs (SDFGs) have proven to be suitable for specifying and analyzing streaming applications that run on single- or multi-processor platforms. Streaming applications essentially continue their execution indefinitely. Therefore, one of the key properties of an SDFG is liveness, i.e., whether all parts of the SDFG can run infinitely often. Another elementary requirement is whether an implementation of an SDFG is feasible using a limited amount of memory. In this paper, we study two interpretations of this property, called boundedness and strict boundedness, that were either already introduced in the SDFG literature or studied for other models. A third and new definition is introduced, namely self-timed boundedness, which is very important to SDFGs, because self-timed execution results in the maximal throughput of an SDFG. Necessary and sufficient conditions for liveness in combination with all variants of boundedness are given, as well as algorithms for checking those conditions. As a by-product, we obtain an algorithm to compute the maximal achievable throughput of an SDFG that relaxes the requirement of strong connectedness in earlier work on throughput analysis

We lay a foundation for modeling and validation of asynchronous designs in a multi-clock synchronous programming model. This allows us to study properties of globally asynchronous systems using synchronous simulation and model-checking toolkits. Our approach can be summarized as automatic transformation of a design consisting of two asynchronously composed synchronous components into a fully synchronous multi-clock model preserving behavioral equivalence. The ultimate goal of this research is to provide the ability to model and build GALS systems in a fully synchronous design framework and deploy it on an asynchronous network preserving all properties of the system proven in the synchronous framework.

While studying the specification of the operational semantics of different programming languages and formalisms, one can observe the following three facts. Firstly, Plotkin's style of structured operational semantics (SOS) has become a standard in defining operational semantics. Secondly, congruence with respect to some notion of bisimilarity is an interesting property for such languages and it is essential in reasoning about them. Thirdly, there are numerous languages that contain an explicit data part in the state of the operational semantics. The first two facts have resulted in a line of research exploring syntactic formats of operational rules to derive the desired congruence property for free. However, the third point (in combination with the first two) is not sufficiently addressed and there is no standard congruence format for operational semantics with an explicit data state. In this paper, we address this problem by studying the implications of the presence of a data state on the notion of bisimilarity. Furthermore, we propose a number of formats for congruence.

Message Sequence Chart (MSC) specifications have found their way into many software engineering methodologies and CASE tools, in particular to represent early life-cycle requirements and high-level design specifications. We analyze iterating and branching MSC specifications with respect to their software architectural content. We present algorithms for the automated synthesis of Real-Time Object-Oriented Modeling (ROOM) models from MSC specifications and discuss their implementation in the MESA toolset.