Abstract The International Competition on Software Verification (SV-COMP) has been an important driver of progress in the formal verification community, fostering tool development, benchmarking, and reproducibility. As the competition grows in scale and complexity, a reproducibility study is essential to evaluate its robustness across environments, uncover hidden dependencies, and ensure long-term sustainability. This work aims to reaffirm the reliability of SV-COMP’s results, provide insights for similar competitions, and facilitate the adoption of its infrastructure beyond the competition. We reproduced the verification and validation results of active participants, including score and ranking calculations for the verification track. We found several problems prohibiting reusability and reproducibility of some participating tools, but we did not find serious issues with the competition infrastructure itself.

Abstract ConcurrentWitness2Testis a violation witness validator for concurrent software. Taking both nondeterminism of data and interleaving-based nondeterminism into account, the tool aims to use the metadata described in the violation witnesses to synthesize an executable test harness. While plagued by some initial challenges yet to overcome, the validation performance ofConcurrentWitness2Testcorroborates the usefulness of the proposed approach.

State machines are used in engineering many types of software-intensive systems. UML State Machines extend simple finite state machines with powerful constructs. Among the many extensions, there is one seemingly simple and innocent language construct that fundamentally changes state machines’ reactive model of computation: doActivity behaviors. DoActivity behaviors describe behavior that is executed independently from the state machine once entered in a given state, typically modeling complex computation or communication as background tasks. However, the UML specification or textbooks are vague about how the doActivity behavior construct should be appropriately used. This lack of guidance is a severe issue as, when improperly used, doActivities can cause concurrent, non-deterministic bugs that are especially challenging to find and could ruin a seemingly correct software design. The Precise Semantics of UML State Machines (PSSM) specification introduced detailed operational semantics for state machines. To the best of our knowledge, there is no rigorous review yet of doActivity's semantics as specified in PSSM. We analyzed the semantics by collecting evidence from cross-checking the text of the specification, its semantic model and executable test cases, and the simulators supporting PSSM. We synthesized insights about subtle details and emergent behaviors relevant to tool developers and advanced modelers. We reported inconsistencies and missing clarifications in more than 20 issues to the standardization committee. Based on these insights, we studied 11 patterns for doActivities detailing the consequences of using a doActivity in a given situation and discussing countermeasures or alternative design choices. We hope that our analysis of the semantics and the patterns help vendors develop conformant simulators or verification tools and engineers design better state machine models.

Abstract Modelling languages play a central role in developing complex, critical systems. A precise, comprehensible, and high-quality modelling language specification is essential to all stakeholders using, implementing, or extending the language. Many good practices can be found that improve the understandability or consistency of the languages’ semantics. However, designing a modelling language intended for a large audience is still challenging. In this paper, we investigate the challenges and typical issues with assessing the specifications of behavioural modelling language semantics. Our key insight is that the various stakeholder’s understandings of the language’s semantics are often misaligned, and the semantics defined in various artefacts (simulators, test suites) are inconsistent. Therefore assessment of semantics should focus on identifying and resolving these inconsistencies. To illustrate these challenges and techniques, we assessed parts of a state-of-the-art specification for a general-purpose modelling language, the Precise Semantics of UML State Machines (PSSM). We reviewed the text of the specification, analysed and executed PSSM’s conformance test suite, and categorised our experiences according to questions generally relevant to modelling languages. Finally, we made recommendations for improving the development of future modelling languages by representing the semantic domain and traces more explicitly, applying diverse test design techniques to obtain conformance test suites, and using various tools to support early-phase language design.

Through the increasing complexity and dynamics of industrial automation scenarios, the notion of Systems of Systems (SoS) has gained importance in this field. Here, interconnected constituent (hardware as well as software) systems collaborate in order to achieve common goals and to increase the efficiency of certain industrial applications.The Arrowhead Tools project aims at proposing a comprehensive, flexible platform for supporting SoS engineering in its every phase, in the form of an engineering toolchain. Thereby, although the SoS operation aspect has been already elaborated on, the design phase and the usage of design artifacts as part of a continous tool interoperability scenario received less attention so far. In this paper, we describe such a toolchain interoperability scenario, paving the way towards an established, integrated solution, by linking systems modeling practices with SoS operational management. In particular, we propose a customtailored abstract SysML profile for Arrowhead SoS design, and a prototype implementation for a bidirectional link between SoS models and a tool for managing Arrowhead SoS via a customtailored textual format. We illustrate the approach through a realistic industrial application.

Context: White-box test generation is a technique used for automatically selecting test inputs using only the code under test. However, such techniques encounter challenges when applying them to complex programs. One of the challenges is handling invocations to external modules or dependencies in the code under test. Objective: Without using proper isolation, like mocks, generated tests cannot cover all parts of the source code. Moreover, invoking external dependencies may cause unexpected side effects (e.g., accessing the file system or network). Our goal was to tackle this issue while maintaining the advantages of white-box test generation. Method: In this paper, we present an automated approach addressing the external dependency challenge for white-box test generation. This technique isolates the test generation and execution by transforming the code under test and creating a parameterized sandbox with generated mocks. We implemented the approach in a ready-to-use tool using Microsoft Pex as a test generator, and evaluated it on 10 open-source projects from GitHub having more than 38.000 lines of code in total. Results: The results from the evaluation indicate that if the lack of isolation hinders white-box test generation, then our approach is able to help: it increases the code coverage reached by the automatically generated tests, while it prevents invoking any external module or dependency. Also, our results act as a unique baseline for the test generation performance of Microsoft Pex on open-source projects. Conclusion: Based on the results, our technique might serve well for handling external dependencies in white-box test generation as it increases the coverage reached in such situations, while maintaining the practical applicability of the tests generated on the isolated code.

Abstract Automated formal verification is often based on the Counterexample-Guided Abstraction Refinement (CEGAR) approach. Many variants of CEGAR have been developed over the years as different problem domains usually require different strategies for efficient verification. This has lead to generic and configurable CEGAR frameworks, which can incorporate various algorithms. In our paper we propose six novel improvements to different aspects of the CEGAR approach, including both abstraction and refinement. We implement our new contributions in the Theta framework allowing us to compare them with state-of-the-art algorithms. We conduct an experiment on a diverse set of models to address research questions related to the effectiveness and efficiency of our new strategies. Results show that our new contributions perform well in general. Moreover, we highlight certain cases where performance could not be increased or where a remarkable improvement is achieved.

Since safety-critical autonomous vehicles need to interact with an immensely complex and continuously changing environment, their assurance is a major challenge. While systems engineering practice necessitates assurance on multiple levels, existing research focuses dominantly on component-level assurance while neglecting complex system-level traffic scenarios. In this paper, we aim to address the system-level testing of the situation-dependent behavior of autonomous vehicles by combining various model-based techniques on different levels of abstraction. (1) Safety properties are continuously monitored in challenging test scenarios (obtained in simulators or field tests) using graph query and complex event processing techniques. To precisely quantify the coverage of an existing test suite with respect regulations of safety standards, (2) we provide qualitative abstractions of causal, temporal, or geospatial data recorded in individual runs into situation graphs, which allows to systematically measure system-level situation coverage (on an abstract level) wrt. safety concepts captured by domain experts. Moreover, (3) we can systematically derive new challenging (abstract) situations which justifiably lead to runtime behavior which has not been tested so far by adapting consistent graph generation techniques, thus increasing situation coverage. Finally, (4) such abstract test cases are concretized so that they can be investigated in a real or simulated context.

White-box test generation analyzes the code of the system under test, selects relevant test inputs, and captures the observed behavior of the system as expected values in the tests. However, if there is a fault in the implementation, this fault could get encoded in the assertions (expectations) of the tests. The fault is only recognized if the developer, who is using test generation, is also aware of the real expected behavior. Otherwise, the fault remains silent both in the test and in the implementation. A common assumption is that developers using white-box test generation techniques need to inspect the generated tests and their assertions, and to validate whether the tests encode any fault or represent the real expected behavior. Our goal is to provide insights about how well developers perform in this classification task. We designed an exploratory study to investigate the performance of developers. We also conducted an internal replication to increase the validity of the results. The two studies were carried out in a laboratory setting with 106 graduate students altogether. The tests were generated in four open-source projects. The results were analyzed quantitatively (binary classification metrics and timing measurements) and qualitatively (by observing and coding the activities of participants from screen captures and detailed logs). The results showed that participants tend to incorrectly classify tests encoding both expected and faulty behavior (with median misclassification rate 20%). The time required to classify one test varied broadly with an average of 2 min. This classification task is an essential step in white-box test generation that notably affects the real fault detection capability of such tools. We recommended a conceptual framework to describe the classification task and suggested taking this problem into account when using or evaluating white-box test generators.

In this paper, we present Theta, a configurable model checking framework. The goal of the framework is to support the design, execution and evaluation of abstraction refinement-based reachability analysis algorithms for models of different formalisms. It enables the definition of input formalisms, abstract domains, model interpreters, and strategies for abstraction and refinement. Currently it contains front-end support for transition systems, control flow automata and timed automata. The built-in abstract domains include predicates, explicit values, zones and their combinations, along with various refinement strategies implemented for each. The configurability of the framework allows the integration of several abstraction and refinement methods, this way supporting the evaluation of their advantages and shortcomings. We demonstrate the applicability of the framework by use cases for the safety checking of PLC, hardware, C programs and timed automata models.

Summary In recent years, several tools have been developed to automatically select test inputs from the code of the system under test. However, each of these tools has different advantages, and there is a little detailed feedback available on the actual capabilities of the various tools. To evaluate test input generators, this paper collects a set of programming language concepts that should be handled by the tools and maps these core concepts and challenging features like handling the environment or multi‐threading to 363 code snippets, respectively. These snippets would serve as inputs for the tools. Next, the paper presents SETTE, an automated framework to execute and evaluate these snippets. Using SETTE, multiple experiments were performed on five Java and one .NET‐based tools using symbolic execution, search‐based, and random techniques. The test suites' coverage, size, generation time, and mutation score were compared. The results highlight the strengths and weaknesses of each tool and approach and identify hard code parts that are difficult to tackle for most of the tools. We hope that this research could serve as actionable feedback to tool developers and help practitioners assess the readiness of test input generation.

In recent years several symbolic execution-based tools have been developed to automatically select relevant test inputs from the source code of the system under test. However, each of these tools has different advantages, and there is no detailed feedback available on the actual capabilities of the various tools. In order to evaluate test input generators we collected a representative set of programming language concepts that should be handled by the tools, mapped them to 300 code snippets that would serve as inputs for the tools, created an automated framework to execute and evaluate these snippets, and performed experiments on four Java and one .NET test generator tools. The results highlight the strengths and weaknesses of each tool, and identify hard code parts that are difficult to tackle for most of the tools. We hope that our research could serve as actionable feedback to tool developers and help practitioners assess the readiness of test input generation.

Generating test inputs from source code is a topic that is starting to transfer from academic research to industrial application. Symbolic execution is one of the promising techniques for such white-box test generation. However, test input generation for non-trivial programs often reaches limitations even when using the most mature tools due to the underlying complexity of the problem. In such cases, visualizing the symbolic execution and the test generation process could help to quickly identify required configurations and modifications that enable the generation of further test inputs and increase coverage. We present a tool that is able to interactively visualize symbolic execution. We also show how this tool can be used for educational and engineering purposes.

Advances in wireless networking have yielded the development of mobile applications. However, sound technology to specify, design and validate such applications is still to be investigated. In order to exemplify some of the challenges that are raised, this paper reports on a case study: a group membership protocol for ad hoc networks. The protocol has been analyzed by reviewing the specification and the code, and then by testing the implementation. The outcomes provides us with hints for research direction.