The verification of dependability and performance requirements plays a critical role during the development of complex heterogeneous system-of-systems in the automotive, transportation, and aerospace domains. The dependability and performability aspects of the system are often analyzed either by manually constructing formal models or by model transformations provided by systems engineering toolchains. However, for system-level dependability and performance verification, various models from multiple formalisms shall be integrated into a single analysis model as heterogeneous system-of-systems development often relies on different engineering languages and toolchains for different components and subsystems. This paper presents a novel approach to integrating various engineering models into a common extra-functional analysis framework. We utilize an existing intermediate formal language to provide formal semantics to the engineering languages and also introduce a language extension to capture the stochastic aspects of the system behavior. We also introduce an efficient simulation-based analysis approach using statistical model checking and Bayesian machine learning. We developed a prototype implementation to support our analysis approach, which enables the integrated evaluation of different architecture models and languages using model transformation. We evaluated our analysis approach and prototype implementation using case studies inspired by aerospace, transportation, and IoT systems.

Abstract Analyzing concurrent programs often involves reasoning about happens-before relations, handled by dedicated SMT theory solvers. Recently, preventative propagation rules have been introduced for consistency models to avoid unnecessary computations. This paper analyses the reproducibility of a recently published paper regarding a conflict-avoiding happens-before propagator. We show that the underlying axioms are insufficient for supporting sequential consistency. We find that the algorithm can leave out constraints on event ordering (even considering the original axioms), impacting the accuracy of verification. We show a simple counterexample to the stability claim in the paper. Two revisions of the algorithm are presented, and a proof on the correctness of these approaches respective of the original axioms is shown. The tool implementing the original algorithm is examined to ascertain how it circumvents wrong results. It is found that it deviates from the published algorithm. We show that an unmodified algorithm (via a patch in the implementing tool) causes incorrect results. We also show that our revised algorithm can be implemented efficiently in an independent verification tool.

Abstract Theta is a model checking framework with a strong emphasis on effectively handling concurrency in software using abstraction refinement algorithms. In SV-COMP 2025, we complement our existing approach (abstraction-aware partial order reduction) for multi-threaded programs with a happens before propagator-based BMC check, expecting a significant increase in performance. We again utilize our portfolio with dynamic algorithm selection from last year, with improvements regarding solver choice and configuration ordering. In this paper, we detail our algorithmic improvements in Theta regarding the verification of concurrent software.

Abstract The increasing complexity of reactive systems can be mitigated with the use of components and composition languages in model-driven engineering. Designing composition languages is a challenge itself as both practical applicability (support for different composition approaches in various application domains), and precise formal semantics (support for verification and code generation) have to be taken into account. In our Gamma Statechart Composition Framework, we designed and implemented a composition language for the synchronous, cascade synchronous and asynchronous composition of statechart-based reactive components. We formalized the semantics of this composition language that provides the basis for generating composition-related Java source code as well as mapping the composite system to a back-end model checker for formal verification and model-based test case generation. In this paper, we present the composition language with its formal semantics, putting special emphasis on design decisions related to the language and their effects on verifiability and applicability. Furthermore, we demonstrate the design and verification functionality of the composition framework by presenting case studies from the cyber-physical system domain.

Abstract Smart cyber-physical systems (CPSs) have complex interaction with their environment which is rarely known in advance, and they heavily depend on intelligent data processing carried out over a heterogeneous and distributed computation platform with resource-constrained devices to monitor, manage and control autonomous behavior. First, we propose a distributed runtime model to capture the operational state and the context information of a smart CPS using directed, typed and attributed graphs as high-level knowledge representation. The runtime model is distributed among the participating nodes, and it is consistently kept up to date in a continuously evolving environment by a time-triggered model management protocol. Our runtime models offer a (domain-specific) model query and manipulation interface over the reliable communication middleware of the Data Distribution Service (DDS) standard widely used in the CPS domain. Then, we propose to carry out distributed runtime monitoring by capturing critical properties of interest in the form of graph queries, and design a distributed graph query evaluation algorithm for evaluating such graph queries over the distributed runtime model. As the key innovation, our (1) distributed runtime model extends existing publish–subscribe middleware (like DDS) used in real-time CPS applications by enabling the dynamic creation and deletion of graph nodes (without compile time limits). Moreover, (2) our distributed query evaluation extends existing graph query techniques by enabling query evaluation in a real-time, resource-constrained environment while still providing scalable performance. Our approach is illustrated, and an initial scalability evaluation is carried out on the MoDeS3 CPS demonstrator and the open Train Benchmark for graph queries.

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.

Formal verification is approaching a point where it will be reliably applicable to embedded software. Even though formal verification can efficiently analyze multi-threaded applications, multi-core processors are often considered too dangerous to use in critical systems, despite the many benefits they can offer. One reason is the advanced memory consistency model of such CPUs. Nowadays, most software verifiers assume strict sequential consistency, which is also the naïve view of programmers. Modern multi-core processors, however, rarely guarantee this assumption by default. In addition, complex processor architectures may easily contain design faults. Thanks to the recent advances in hardware verification, these faults are increasingly visible and can be detected even in existing processors, giving an opportunity to compensate for the problem in software. In this paper, we propose a generic approach to consider inconsistent behavior of the hardware in the analysis of software. Our approach is based on formal methods and can be used to detect the activation of existing hardware faults on the application level and facilitate their mitigation in software. The approach relies heavily on recent results of model checking and hardware verification and offers new, integrative research directions. We propose a partial solution based on existing model checking tools to demonstrate feasibility and evaluate their performance in this context.

In safety-critical cyber-physical systems (CPS), a service failure may result in severe financial loss or damage in human life. Smart CPSs have complex interaction with their environment which is rarely known in advance, and they heavily depend on intelligent data processing carried out over a heterogeneous computation platform and provide autonomous behavior. This complexity makes design time verification infeasible in practice, and many CPSs need advanced runtime monitoring techniques to ensure safe operation. While graph queries are a powerful technique used in many industrial design tools of CPSs, in this paper, we propose to use them to specify safety properties for runtime monitors on a high-level of abstraction. Distributed runtime monitoring is carried out by evaluating graph queries over a distributed runtime model of the system which incorporates domain concepts and platform information. We provide a semantic treatment of distributed graph queries using 3-valued logic. Our approach is illustrated and an initial evaluation is carried out using the MoDeS3 educational demonstrator of CPSs.

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.

Stochastic Petri nets are widely used for the modeling and analysis of non-functional properties of critical systems. The state space explosion problem often inhibits the numerical analysis of such models. Symbolic techniques exist to explore the discrete behavior of even complex models, while block Kronecker decomposition provides memory-efficient representation of the stochastic behavior. However, the combination of these techniques into a stochastic analysis approach is not straightforward. In this paper we integrate saturation-based symbolic techniques and decomposition-based stochastic analysis methods. Saturation-based exploration is used to build the state space representation and a new algorithm is introduced to efficiently build block Kronecker matrix representation to be used by the stochastic analysis algorithms. Measurements confirm that the presented combination of the two representations can expand the limits of previous approaches.

PetriDotNet is an extensible Petri net editor and analysis tool originally developed to support the education of formal methods. The ease of use and simple extensibility fostered more and more algorithmic developments. Thanks to the continuous interest of developers (especially M.Sc. and Ph.D. students who choose PetriDotNet as the framework of their thesis project), by now PetriDotNet became an analysis platform, providing various cutting-edge model checking algorithms and stochastic analysis algorithms. As a result, industrial application of the tool also emerged in recent years. In this paper we overview the main features and the architecture of PetriDotNet , and compare it with other available tools.

Abstract Efficient symbolic and explicit-state model checking approaches have been developed for the verification of linear time temporal logic (LTL) properties. Several attempts have been made to combine the advantages of the various algorithms. Model checking LTL properties usually poses two challenges: one must compute the synchronous product of the state space and the automaton model of the desired property, then look for counterexamples that is reduced to finding strongly connected components (SCCs) in the state space of the product. In case of concurrent systems, where the phenomenon of state space explosion often prevents the successful verification, the so-called saturation algorithm has proved its efficiency in state space exploration. This paper proposes a new approach that leverages the saturation algorithm both as an iteration strategy constructing the product directly, as well as in a new fixed-point computation algorithm to find strongly connected components on-the-fly by incrementally processing the components of the model. Complementing the search for SCCs, explicit techniques and component-wise abstractions are used to prove the absence of counterexamples. The resulting on-the-fly, incremental LTL model checking algorithm proved to scale well with the size of models, as the evaluation on models of the Model Checking Contest suggests.

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.

Formal verification is becoming a fundamental step of safety-critical and model-based software development. As part of the verification process, model checking is one of the current advanced techniques to analyze the behavior of a system. In this paper, we examine an existing parallel model checking algorithm and we propose improvements to eliminate some computational bottlenecks. Our measurements show that the resulting new algorithm has better scalability and performance than both the former parallel approach and the sequential algorithm.