Abstract Automated robotic systems operating in real-world environments require thorough test campaigns before deployment, in which engineers assess whether the system is actually exposed to critical scenarios. A well-established way to judge the efficacy of test campaigns in controlled environments is scenario coverage: It quantifies the quality of recorded data from test campaigns w.r.t. a set of (critical) scenario classes of interest. Challenges arise when transferring coverage from controlled to open environments, as it may no longer be exactly determined to which scenario class the recorded test data belongs to: sensors offer limited observability, e.g., by occlusions or hardware failures, and specifications might be inherently vague, e.g., via imprecise traffic regulations. We leverage the Open World Assumption to formally extend scenario coverage to such ambiguous test data and present algorithms for computing guaranteed lower and upper bounds on coverage. Whereas deciding the lower bound problem is $$D^p$$ D p -complete, the upper bound can be computed in polynomial time. We extend an existing coverage software tool with two approaches for incorporating the Open World Assumption, grounded in LTL f . Our evaluation shows that meaningful statements on scenario coverage are feasible, even under intricacies of the real world.

Abstract Existing active automata learning (AAL) algorithms have demonstrated their potential in capturing the behavior of complex systems (e.g., in analyzing network protocol implementations). The most widely used AAL algorithms generate finite state machine models, such as Mealy machines or deterministic finite automata. For many analysis tasks, however, it is crucial to generate richer classes of models that also show how relations between data parameters affect system behavior. Such models have shown potential to uncover critical bugs, but their learning algorithms do not scale beyond small and well curated experiments. In this article, we present $${SL}^{\lambda }$$ SL λ , an effective and scalable register automata (RA) learning algorithm that significantly reduces the number of membership queries required for inferring models. It achieves this by combining a tree-based cost-efficient data structure with mechanisms for computing short and restricted tests. We prove that $${SL}^{\lambda }$$ SL λ is guaranteed to learn an acceptor, in the form of a register automaton with n locations and t transitions, for a given data language of finite index, and that it can do so with at most $$O(t^2 \, (2n)^n + m t^2 \, m^m)$$ O ( t 2 ( 2 n ) n + m t 2 m m ) membership queries and O ( t ) equivalence queries, where m is the length of the longest counterexample received during learning. We have implemented $${SL}^{\lambda }$$ SL λ as a new algorithm in RALib. We evaluate its performance by comparing it against $${SL}^{*}$$ SL ∗ , the current state-of-the-art RA learning algorithm. Experiments on a series of benchmarks show that it reduces the number of membership queries by up to an order of magnitude, and also shows substantial asymptotic improvements in bigger systems.

Abstract In 2015, LearnLib, the open-source framework for active automata learning, received the prestigious CAV artifact award. This paper presents the advancements made since then, highlighting significant additions to LearnLib, including state-of-the-art algorithms, novel learning paradigms, and increasingly expressive models. Our efforts to mature and maintain LearnLib have resulted in its widespread use among researchers and practitioners alike. A key factor in its success is the achieved compositionality which allows users to effortlessly construct thousands of customized learning processes tailored to their specific requirements. This paper illustrates these features through the development of a learning process for the life-long learning of procedural systems. This development can be easily replicated and modified using the latest public release of LearnLib.

We present a post-hoc approach for scenario-based testing of automated driving systems, enabling the analysis of safety and correctness for (cooperative) automated driving systems in many scenarios without conducting tests for individual scenarios. The system under test is operated in its physical environment’ and data is recorded during operation. Then, driving scenarios are identified in this data and functional requirements are checked, yielding pass or fail verdicts for individual scenarios. We validate the envisioned post-hoc approach in a single-case mechanism experiment by the example of a platooning controller, identifying a previously unknown bug in the tested system, as well as a functional insufficiency concerning the intended operational design domain.

Abstract Existing active automata learning (AAL) algorithms have demonstrated their potential in capturing the behavior of complex systems (e.g., in analyzing network protocol implementations). The most widely used AAL algorithms generate finite state machine models, such as Mealy machines. For many analysis tasks, however, it is crucial to generate richer classes of models that also show how relations between data parameters affect system behavior. Such models have shown potential to uncover critical bugs, but their learning algorithms do not scale beyond small and well curated experiments. In this paper, we present $${SL}^{\lambda }$$ SL λ , an effective and scalable register automata (RA) learning algorithm that significantly reduces the number of tests required for inferring models. It achieves this by combining a tree-based cost-efficient data structure with mechanisms for computing short and restricted tests. We have implemented $${SL}^{\lambda }$$ SL λ as a new algorithm in RALib. We evaluate its performance by comparing it against $${SL}^{*}$$ SL ∗ , the current state-of-the-art RA learning algorithm, in a series of experiments, and show superior performance and substantial asymptotic improvements in bigger systems.

The robot operating system 2 (ROS 2) is a widely used collection of tools and libraries for building robot applications. It is designed to be flexible and easy to use when creating complex robot systems with many interacting components.Since its alpha version release in 2015, ROS 2 provides two options in a multithreading operating system, namely the single-threaded executor and the multithreaded executor. The single-threaded executor is starvation-free by design (i.e., every task is eventually executed) even in over-utilized systems, since the set of eligible task instances (called wait set) is only refilled once all the task instances in the wait set are executed. The multithreaded executor extends this mechanism to multiple threads that manage the wait set collaboratively. While intuitively this extension preserves the starvation-free property, and analyses for the multithreaded executor even build upon this assumption, the multithreaded executor has not been shown to be starvation-free.In this work, we examine the mechanism of the multithreaded executor in ROS 2 and demonstrate that it is prone to starvation, i.e., some tasks may never be executed even in under-utilized systems. This indicates risks for multithreaded executors in the current ROS 2 design and further leads to counterexamples to the state-of-the-art response-time analyses by Jiang et al. (RTSS 2022) and Sobhani et al. (RTAS 2023). We propose a minimal change in the software architecture of the ROS 2 multithreaded executor to enable starvation- and deadlock-free behavior. We empirically test that we prevent starvation in concrete ROS 2 system configurations, and show that our solution incurs a negligible overhead using the autoware reference benchmark. Moreover, we prove that our solution is starvation- and deadlock-free using formal proofs and model checking.

Data sovereignty, the possibility to keep control over data, is gaining increasing attention in both research and industry. Due to complex supply chains and a strong trend toward digitization, digital assets are essential to be fast and competitive. As a result, companies need to share data while retaining control over it to prevent unwanted leaks of sensitive data. However, implementing effective data governance, access, and usage control mechanisms can be challenging, especially in cross-company data sharing networks and ecosystems like dataspaces. In this paper, we examine the industrial landscape and interview eleven experts from software providers and producing organizations to identify their requirements and challenges of existing data sovereign solutions. Based on Grounded Theory and semi-structured interviews, we explore the motivations and issues behind data sharing from an Information Systems and Software Engineering point of view. The findings include current industrial contexts, use cases, and solutions with data sovereignty’s technical and non-technical implementations. Seven requirements and thirteen challenges were observed throughout a qualitative analysis. Clustered by organizational, technical, personal, and emotional viewpoints, they are discussed with initial approaches for mitigation. The results identify current practical needs and will enable the design of future data sovereignty solutions in theory and different practical domains.

In recent years, scenario-based testing has gained increased attention as a potentially efficient strategy for validating the overall safety of automated vehicles. However, which scenarios are of interest for testing and how to systematically generate the test instances remain as unanswered questions. In this work, we interpret the importance of incorporating automated vehicle disengagement scenarios into scenario-based testing. Accordingly, we design and implement a fully automatic pipeline to reconstruct the essential and error-reduced disengagement scenarios based on imperfect perception measurement data from real test drives in an urban environment. Our concept is developed based on 137 disengagement data snippets and two additional datasets for handling false positives and false negatives in the original measurements. We use additional disengagement snippets for validating the performance of the pipeline. We exhibit representative reconstructed scenarios to show a successful restoration of the reality and quantitatively demonstrate the correct functioning of the methods in the pipeline regarding filtering irrelevant objects and handling the perception inaccuracies.

The establishment of collaborative AI pipelines, in which multiple organizations share their data and models, is often complicated by lengthy data governance processes and legal clarifications. Data sovereignty solutions, which ensure data is being used under agreed terms and conditions, are promising to overcome these problems. However, there is limited research on their applicability in AI pipelines. In this study, we extended an existing AI pipeline at Mondragon Corporation, in which sensor data is collected and subsequently forwarded to a data quality service provider with a data sovereignty component. By systematically reflecting and generalizing our experiences during the twelve-month action research project, we formulated ten lessons learned, four benefits, and three barriers to data-sovereign AI pipelines that can inform further research and custom implementations. Our results show that a data sovereignty component can help reduce existing barriers and increase the success of collaborative data science initiatives.

To achieve safety of high level automated driving, not only functional failures like E/E system malfunctions and software crashes should be excluded, but also functional insufficiencies and performance limitations such as sensor resolution should be thoroughly investigated and considered. The former problem is known as functional safety (FuSa), which is coped with by ISO 26262. The latter focuses on safe vehicle behavior and is summarized as safety of the intended functionality (SOTIF) within the under development standard ISO 21448. For realizing this safety level, it is crucial to understand the system and the triggering conditions that activate its existing functional insufficiencies. However, the concept of triggering condition is new and still lacks relevant research. In this paper, we interpret triggering condition and other SOTIF-relevant terms in the scope of ISO 21448. We summarize the formal formulations of triggering conditions based on several key principles and provide possible categories for facilitating the systematization. We contribute a novel method for the identification of triggering conditions and offer a comparison with two other proposed methods regarding diverse aspects. Furthermore, we show that our method requires less insight into the system and fewer brainstorm efforts and provides well-structured and distinctly formulated triggering conditions.

Abstract GWIT is a validator for violation witnesses produced by Java verifiers in the SV-COMP software verification competition. GWIT weaves assumptions documented in a witness into the source code of a program, effectively restricting the part of the program that is explored by a program analysis. It then uses the GDart tool (dynamic symbolic execution) to search for reachable errors in the modified program.

Abstract GDart is an ensemble of tools allowing dynamic symbolic execution of JVM programs. The dynamic symbolic execution engine is decomposed into three different components: a symbolic decision engine (DSE), a concolic executor (SPouT), and a SMT solver backend allowing meta-strategy solving of SMT problems (JConstraints). The symbolic decision component is loosely coupled with the executor by a newly introduced communication protocol. At SV-COMP 2022, GDart solved 471 of 586 tasks finding more correct false results (302) than correct true results (169). It scored fourth place.

Data forms an essential organizational asset and is a potential source for competitive advantages. To exploit these advantages, the engineering of data-intensive applications is becoming increasingly important. Yet, the professional development of such applications is still in its infancy and a practical engineering approach is necessary to reach the next maturity level. Therefore, resources and frameworks that bridge the gaps between theory and practice are required. In this study, we developed a data engineering reference model (DERM), which outlines the important building-blocks for handling data along the data lifecycle. For the creation of the model, we conducted a systematic literature review on data lifecycles to find commonalities between these models and derive an abstract meta-model. We successfully validated our model by matching it with established data engineering topics. Using the model derived six research gaps that need further attention for establishing a practically-grounded engineering process. Our model will furthermore contribute to a more profound development process within organizations and create a common ground for communication.

Many modern software engineering tools integrate SMT decision procedures and rely on the accuracy and performance of SMT solvers. We describe four basic patterns for integrating constraint solvers (earliest verdict, majority vote, feature-based solver selection, and verdict-based second attempt) that can be used for combining individual solvers into meta-decision procedures that balance accuracy, performance, and cost – or optimize for one of these metrics. In order to evaluate the effectiveness of meta-solving, we analyze and minimize 16 existing benchmark suites and benchmark seven state-of-the-art SMT solvers on 17k unique instances. From the obtained performance data, we can estimate the performance of different meta-solving strategies. We validate our results by implementing and analyzing two strategies. As additional results, we obtain (a) the first benchmark suite of unique SMT string problems with validated expected verdicts, (b) an extensive dataset containing data on benchmark instances as well as on the performance of individual decision procedures and several meta-solving strategies on these instances, and (c) a framework for generating data that can easily be used for similar analyses on different benchmark instances or for different decision procedures.

Abstract JDartperforms dynamic symbolic execution ofJavaprograms: it executes programs with concrete inputs while recording symbolic constraints on executed program paths. A portfolio of constraint solvers is then used for generating new concrete values from recorded constraints that drive execution along previously unexplored paths. For SV-COMP 2021, we improvedJDartby implementing exploration strategies, bounded analysis, and path-specific constraint solving strategies, as well as by enabling the use of SMT-Lib string theory for encoding of string operations.

Abstract This paper (1) summarizes the history of the RERS challenge for the analysis and verification of reactive systems, its profile and intentions, its relation to other competitions, and, in particular, its evolution due to the feedback of participants, and (2) presents the most recent development concerning the synthesis of hard benchmark problems. In particular, the second part proposes a way to tailor benchmarks according to the depths to which programs have to be investigated in order to find all errors. This gives benchmark designers a method to challenge contributors that try to perform well by excessive guessing.

IT security is an important aspect of system design and of quality assurance during the software engineering process. Today, there is a big demand for IT security specialists in job markets around the world. Increased automation of security code reviews is one approach for mitigating the current shortage of IT security professionals. We designed the course “Formal Methods for IT Security” to teach undergraduate students the basics of constraint solving and formal modeling techniques suitable for automation of IT security code reviews in a hands-on format. In this paper, we describe the didactic concept of the course along with the required modifications due to the COVID-19 pandemic. Further, we report our experience from remote teaching the class during the summer term affected by the pandemic. The main pandemic-related challenge we tackled during the course is establishing communication and stimulation of the discussions required for learning in projects without any presence meetings.

31

Abstract JDart performs dynamic symbolic execution of Java programs: it executes programs with concrete inputs while recording symbolic constraints on executed program paths. A constraint solver is then used for generating new concrete values from recorded constraints that drive execution along previously unexplored paths. JDart is built on top of the Java PathFinder software model checker and uses the JConstraints library for the integration of constraint solvers.

This paper covers the Rigorous Examination of Reactive Systems (RERS) Challenge 2019. For the first time in the history of RERS, the challenge features industrial tracks where benchmark programs that participants need to analyze are synthesized from real-world models. These new tracks comprise LTL, CTL, and Reachability properties. In addition, we have further improved our benchmark generation infrastructure for parallel programs towards a full automation. RERS 2019 is part of TOOLympics, an event that hosts several popular challenges and competitions. In this paper, we highlight the newly added industrial tracks and our changes in response to the discussions at and results of the last RERS Challenge in Cyprus.

RERS is an annual verification challenge that focuses on LTL and reachability properties of reactive systems. In 2017, RERS was extended to a one day workshop that in addition to the original challenge program also featured an invited talk about possible future developments. As a satellite of ISSTA and SPIN, the 2017 RERS Challenge itself increased emphasis on the parallel benchmark problems which, like their sequential counterparts, were generated using property-preserving transformations in order to scale their level of difficulty. The first half of the RERS workshop focused on the 2017 benchmark profiles, the evaluation of the received contributions, and short presentations of each participating team. The second half comprised discussions about attractive problem scenarios for future benchmarks, like race detection, the topic of the invited talk, and about systematic ways to leverage a tool's performance based on competition benchmarks and machine learning.

Abstract We present a black-box active learning algorithm for inferring extended finite state machines (EFSM)s by dynamic black-box analysis. EFSMs can be used to model both data flow and control behavior of software and hardware components. Different dialects of EFSMs are widely used in tools for model-based software development, verification, and testing. Our algorithm infers a class of EFSMs called register automata . Register automata have a finite control structure, extended with variables (registers), assignments, and guards. Our algorithm is parameterized on a particular theory , i.e., a set of operations and tests on the data domain that can be used in guards. Key to our learning technique is a novel learning model based on so-called tree queries . The learning algorithm uses tree queries to infer symbolic data constraints on parameters, e.g., sequence numbers, time stamps, identifiers, or even simple arithmetic. We describe sufficient conditions for the properties that the symbolic constraints provided by a tree query in general must have to be usable in our learning model. We also show that, under these conditions, our framework induces a generalization of the classical Nerode equivalence and canonical automata construction to the symbolic setting. We have evaluated our algorithm in a black-box scenario, where tree queries are realized through (black-box) testing. Our case studies include connection establishment in TCP and a priority queue from the Java Class Library.

The Next Generation Air Transportation System (NextGen) advocates the use of innovative algorithms and software to address the increasing load on air-traffic control. AutoResolver [12] is a large, complex NextGen component that provides separation assurance between multiple airplanes up to 20 minutes ahead of time. Our work targets the development of a light-weight, automated testing environment for AutoResolver. The input space of AutoResolver consists of airplane trajectories, each trajectory being a sequence of hundreds of points in the three-dimensional space. Generating meaningful test cases for AutoResolver that cover its behavioral space to a satisfactory degree is a major challenge. We discuss how we tamed this input space to make it amenable to test case generation techniques, as well as how we developed and validated an extensible testing environment around AutoResolver.

This paper addresses the problem of efficient generation of component interfaces through learning. Given a white-box component C with specified unsafe states, an interface captures safe orderings of invocations of C's public methods. In previous work we presented Psyco, an interface generation framework that combines automata learning with symbolic component analysis: learning drives the framework in exploring different combinations of method invocations, and symbolic analysis computes method guards corresponding to constraints on the method parameters for safe execution. In this work we propose solutions to the two main bottlenecks of Psyco. The explosion of method sequences that learning generates to validate its computed interfaces is reduced through partial order reduction resulting from a static analysis of the component. To avoid scalability issues associated with symbolic analysis, we propose novel algorithms that are primarily based on dynamic, concrete component execution, while resorting to symbolic analysis on a limited, as needed, basis. Dynamic execution enables the introduction of a concept of state matching, based on which our proposed approach detects, in some cases, that it has exhausted the exploration of all component behaviors. On the other hand, symbolic analysis is enhanced with symbolic summaries. Our new approach, X-Psyco, has been implemented in the Java PathFinder (JPF) software model checking platform. We demonstrated the effectiveness of X-Psyco on a number of realistic software components by generating more complete and precise interfaces than was previously possible.