This special collection arose from the 18th International Conference on integrated Formal Methods (iFM 2023), which was held in Leiden, The Netherlands from 13 to 15 November 2023.

Embedded systems are used in many safety-critical domains, including in medicine, traffic, and critical infrastructure. Due to the strict timing requirements such systems usually have to fulfill, they often run on real-time operating systems (RTOS). As the RTOS influences the function and the timing behavior of the system, it becomes important to rigorously ensure the correctness and safety of applications running on them while taking into account the semantics of the operating system. Existing verification approaches are either limited to specific RTOS components or based on explicit state space exploration techniques such as model checking, which do not scale well for concurrent or timed applications. In this article, we propose a deductive approach to verify crucial safety properties about applications written for the widely-used RTOS FreeRTOS using the VerCors verifier. Our key ideas are threefold: (1) We provide a formalization of a wide variety of FreeRTOS features and an automatic encoding of FreeRTOS applications for verification with VerCors. (2) We adapt and enhance an existing approach for automatic invariant generation to largely automate the typically high-effort verification process. (3) We present a systematic technique to verify both functional and timing-related properties of cooperative RTOS applications. We demonstrate the applicability of our approach on a FreeRTOS demo application as well as an adaptive cruise control system.

Abstract Autonomous hybrid systems are systems that combine discrete and continuous behavior with autonomous decision-making, e.g., using reinforcement learning. Such systems are increasingly used in safety-critical applications such as self-driving cars, autonomous robots or water supply systems. Thus, it is crucial to ensure their safety and resilience, i.e., that they function correctly even in the presence of dynamic changes and disruptions. In this paper, we present an approach to obtain formal resilience guarantees for autonomous hybrid systems using the interactive theorem prover KeYmaera X. Our key ideas are threefold: First, we derive a formalization of resilience that is tailored to autonomous hybrid systems. Second, we present reusable patterns for modeling stressors, detecting disruptions, and specifying resilience as a service level response in the differential dynamic logic (d $$\mathcal {L}$$ L ). Third, we combine these concepts with an existing approach for the safe integration of learning components using hybrid contracts, and extend it towards dynamic adaptations to stressors. By combining reusable patterns for stressors, observers, and adaptation contracts for learning components, we provide a systematic approach for the deductive verification of resilience of autonomous hybrid systems with reduced specification effort. We demonstrate the applicability of our approach with two case studies, an autonomous robot and an intelligent water distribution system.

Finding test-cases that cause mission-critical behavior is crucial to increase the robustness of satellite on-board image processing. Using genetic algorithms, we are able to automatically search for test cases that provoke such mission-critical behavior in a large input domain. However, since genetic algorithms generate new test cases using random mutations and crossovers in each generation, they do not provide an explanation why certain test cases are chosen. In this paper, we present an approach to increase the explainability of genetic test generation algorithms using principal component analysis together with visualizations of its results. The analysis gives deep insights into both the system under test and the test generation. With that, the robustness can be significantly increased because we 1) better understand the system under test as well as the selection of certain test cases and 2) can compare the generated explanations with the expectations of domain experts to identify cases with unexpected behavior to identify errors in the implementation. We demonstrate the applicability of our approach with a satellite on-board image processing application.

Abstract In embedded systems, the execution semantics of the real-time operating system (RTOS), which is responsible for scheduling and timely execution of concurrent processes, is crucial for the correctness of the overall system. However, existing approaches for the formal verification of embedded systems typically abstract from the RTOS completely, or provide a detailed and synthesizable formal model of the RTOS. While the former may lead to unsafe systems, the latter is not compatible with industrial design processes. In this paper, we present an approach for reusable abstract formal models that can be configured for custom RTOS. Our key idea is to formally capture common execution mechanisms of RTOS like preemptive scheduling, event synchronization, and communication abstractly in configurable timed automata models. These abstract formal models can be configured for a concrete custom RTOS, and they can be combined into a formal system model together with a concrete application. Our reusable models significantly reduce the manual effort of defining a formal model that captures concurrency and real-time behavior, together with the functionality of an application. The resulting formal model enables analysis, verification, and graphical simulation. We validate our approach by formalizing and analyzing a rescue robot application running the custom open source RTOS EV3RT.

Simultaneous localization and mapping (SLAM) is a prerequisite for accurate navigation of autonomous vehicles. Although this is often safety- critical, systematic approaches for testing the correctness and accuracy of SLAM algorithms are missing. In this paper, we present an approach for automated and systematic testing of SLAM algorithms. We identify challenging environmental features for SLAM, define coverage criteria that characterize the SLAM problem’s input space, and develop a method for automatically generating high-coverage tests. We demonstrate the effectiveness of our approach with a case study on an existing FastSLAM implementation.

Satellite on-board image processing technologies are subject to extremely strict requirements with respect to reliability and accuracy in hard real-time. In this paper, we address the problem of automatically selecting test cases that are specifically tailored to provoke mission-critical behavior of satellite on-board image processing applications. Because such applications possess large input domains, it is infeasible to exhaustively execute all possible test cases. In particular, because of their complex computations, it is difficult to find specific test cases that provoke mission-critical behavior. To overcome this problem, we define a test approach that is based on a genetic algorithm. The goal is to automatically generate test cases that provoke worst case execution times and inaccurate results of the satellite on-board image processing application. For this purpose, we define a two-criteria fitness function that is novel in the satellite domain. We show the efficiency of our test approach on experimental results from the Fine Guidance System of the ESA medium-class mission PLATO.

Embedded systems often consist of deeply intertwined hardware and software components. At the same time, they are often used in safety-critical applications, where an error may result in enormous costs or even loss of human lives. Existing verification techniques that show the absence of errors do not scale well for complex integrated HW/SW systems. In this paper, we present a dependence analysis and automated partitioning approach for the formal analysis of HW/SW codesigns that are modeled in SystemC. The key idea of our approach is threefold: first, we partition a given system into loosely coupled submodels. Second, we analyze the dependences between these submodels and compute an abstract verification interface for each of them, which captures all possible influences of all other submodels. Third, we verify global properties of the overall system by verifying them separately for each subsystem. We demonstrate that our approach significantly reduces verification times and increases scalability with results for an anti-lock braking system.

The efficient mapping of stream processing applications to parallel hardware architectures is a difficult problem. While parallelization is often highly desirable as it reduces the overall execution time, its advantages must be carefully weighed against the parallelization overhead of complexity and communication costs. This paper presents a novel profile-guided optimization for parallel stream processing based on the multi-paradigm system programming language Rust. Our approach's key idea is to systematically balance the performance gain that can be achieved from parallelization with the communication overhead. To achieve this, we 1) use profiling to gain tight estimates of task execution times, 2) evaluate the cost of the fundamental concurrency constructs in Rust with synthetic benchmarks, and exploit this information to estimate the communication overhead introduced by various degrees of parallelism, and 3) present a novel optimization algorithm that exploits both estimates to fine-tune the degree of parallelism and train processing in a given application. Overall, our approach enables us to map parallel stream processing applications to parallel hardware efficiently. The safety concepts anchored in Rust ensure the reliability of the resulting implementation. We demonstrate our approach's practical applicability with two case studies: the word count problem and aircraft telemetry decoding.

Side-channel attacks (SCA) enable attackers to gain access to non-disclosed information by measuring emissions of a system, for example, electromagnetic waves or power consumption. In existing design processes, the emissions of a system can only be measured on the final system. As a consequence, the analysis of such security threats is often only possible at a very late stage in the development process. In this paper, we present an approach to simulate power attacks in early stages of the development process. The key idea of our approach is threefold: First, we use the powerful system level design language SystemC to provide a detailed model of the power consumption of a given system. Second, we provide a graphical user interface to visualize and analyze the power consumption. Third, we develop predefined attacker modules in SystemC. Together, we provide a framework to simulate and analyze whether known power attacks are successful on a given system. We demonstrate the applicability of our approach by modeling and simulating a simple power attack (SPA) on a system that uses elliptic curve cryptography (ECC), a differential power attack on a system that uses RSA encryption, and a cross-correlation analysis on the same system.

Embedded systems are often used in safety-critical applications like cars or airplanes. This makes it crucial to verify their hardware and software under all circumstances. In previous work, we have presented an approach for the formal verification of integrated hardware/software systems using the satisfiability modulo theory solving based verification system UCLID. However, the transformation of integrated hardware/software systems into the input language of the UCLID verification system causes a considerable overhead in the number of symbolic simulation steps necessary for k-inductive verification. In this paper, we overcome this problem by presenting two optimizations for the symbolic simulation of cooperatively scheduled concurrent processes: First, we realize a reduction of redundant states in individual functions that respects all data, control and inter-process dependencies. To capture these dependencies precisely, we present the novel concept of a cooperative dominator tree, which extends the classical concept of a dominator tree to cooperatively scheduled concurrent processes. Second, we present a process parallelization for cooperatively scheduled concurrent processes based on a SystemC dependence graph. In our evaluation based on a set of 21 synthetic case studies, we reach an average reduction of the inductive verification times by 40 %.

On-board image processing technologies in the satellite domain are subject to extremely strict requirements with respect to reliability and accuracy in hard real-time. Due to their large input domain, it is infeasible to execute all possible test cases. To overcome this problem, we define a novel test approach that efficiently and systematically captures the input domain of satellite on-board image processing applications. To achieve this, we first present a dedicated partitioning into equivalence classes for each input parameter. Then, we define multidimensional coverage criteria to assess a given test suite for its coverage on the complete input domain. Finally, we present a test generation algorithm that automatically inserts missing test cases into a given test suite based on our multidimensional coverage criteria. This results in a reasonably small test suite that covers the whole input domain of satellite on-board image processing applications. We demonstrate the effectiveness of our approach with experimental results from the ESA medium-class mission PLATO.

Writing correct and efficient parallel programs is hard. A lack of overview leads to errors in control- and dataflow, e.g., race conditions, which are hard to find due to their nondeterministic nature. In this paper, we present a graphical programming model for parallel stream processing applications, which improves the overview by visualizing high level dataflow together with explicit and concise annotations for concurrency-related dependency information. The key idea of our approach is twofold: First, we present a powerful graphical task editor together with annotations that enable the designer to define stream properties, task dependencies, and routing information. These annotations facilitate fine-granular and correct parallelization. Second, we propose seamless integration with the safe parallel programming language Rust by providing automated code structure generation from the graphical representation, design patterns for common parallel programming constructs like filters, and a scheduling and runtime environment. We demonstrate the applicability of our approach with a network-based processing system as it is typically found in advanced firewalls.

Simulink and Stateflow are widely-used industrial tools for the development of embedded systems, e.g. in the automotive domain. In modern automotive control systems, multiple components are typically interconnected, and, nowadays, also have a connection to the internet. This poses severe threats, as safety-critical components may be subject to remote attacks, which divert control or information flow from non-critical to safety-critical components. In this paper, we present a novel approach for the analysis of information flow in combined Simulink/Stateflow models. The key idea of our approach is that we analyze the information flow in a given model by computing an over-approximation of the control flow and deduce whether all control flow conditions on a given path combined permit information flow or not. With our approach, we safely rule out the existence of information flow on specific paths. Thus, it enables us to reason about non-interference and the compliance with security policies.

Approaches for the automatic analysis of security policies on source code level cannot trivially be applied to binaries. This is due to the lacking high-level semantics of low-level object code, and the fundamental problem that control-flow recovery from binaries is difficult. We present a novel approach to recover the control-flow of binaries that is both safe and efficient. The key idea of our approach is to use the information contained in security mechanisms to approximate the targets of computed branches. To achieve this, we first define a restricted control transition intermediate language (RCTIL), which restricts the number of possible targets for each branch to a finite number of given targets. Based on this intermediate language, we demonstrate how a safe model of the control flow can be recovered without data-flow analyses. Our evaluation shows that that makes our solution more efficient than existing solutions.

Simulink is widely used in model-driven design.However, the complexity of hybrid systems that are modeled in Simulink limits the applicability of reuse techniques, which impedes cost-efficient design of complex systems. In particular, a systematic use and reuse of complex submodels, e.g. components with varying structure and functionality, is currently not supported. In this paper, we present an approach for service-oriented design in Simulink. The main idea is that we create a modular representation of complex Simulink structures as services with an expressive and formally defined dynamic interface. A dynamic interface captures not only the types of input and output signals but also their discrete and continuous behavior. Our main contribution is threefold: First, we introduce services in Simulink. Second, we transfer the concept of feature modeling to Simulink to express the variability of a service. Third, we introduce the novel concept of hybrid contracts to define the dynamic interface of a service. With our approach, we enable the designer (1) to define hybrid services that are reusable, and (2) to efficiently develop complex hybrid systems from a given set of services. We demonstrate this with a case study of a hybrid temperature control system.

Current anomaly detection systems that enforce control flow integrity based on control flow graph information are not able to precisely monitor dynamic aspects of execution. Consequently, they are typically too coarse-grained to comprehensively detect modern code-reuse attacks. Even when enriched with dynamic monitoring information such as shadow stacks, the heuristics used are either too imprecise or produce many false negatives. In this paper, we present a novel approach to establish control flow integrity in multi-variant execution through execution location equivalence. The concept of execution location equivalence allows us to precisely detect execution divergence using a diversified control flow model and, consequently, to detect a broad variety of code-reuse attacks. In this way, execution of position-independent executables can be reliably rotected against a broad range of control hijacking attacks.

Understanding the behavior of a program when no source code is available tends to be a complicated and time-expensive task. In particular, only very limited information can be gained without analyzing the binary's assembler representation. In this paper, we present a novel approach for reverse engineering of ARM binaries. The main idea is to translate the original assembler representation into a formal intermediate representation language, namely WSL, and then to apply rephrasing transformations to the code. To achieve a highly modular translation, we define a rule set to translate each assembler instruction individually. Furthermore, new rephrasing rules were developed to recover high level control flow aspects and to eliminate assembler specific program fragments in the intermediate code. Our translation engine was coupled with the FermaT program transformation system to apply the rephrasing rules. We demonstrate the applicability of our approach through the successful recovery of high level control flow statements in the Debian coreutils binaries. Using these example binaries, we studied the performance and the quality of our transformation.

Matlab/Simulink is widely used for model-based development of embedded systems. In particular, safety-critical applications are increasingly designed in Matlab/Simulink. At the same time, formal verification techniques for Matlab/Simulink are still rare and existing ones do not scale well. In this paper, we present an automatic transformation from discrete-time Matlab/Simulink to the input language of UCLID. UCLID is a toolkit for system verification based on SMT solving. Our approach enables us to use a combination of bounded model checking and inductive invariant checking for the automatic verification of Matlab/Simulink models. To demonstrate the practical applicability of our approach, we have successfully verified the absence of one of the most common errors, i. e. variable over- or underflow, for an industrial design from the automotive domain.

SystemC is widely used for modeling and simulation in hardware/software co-design. However, existing verification techniques are mostly ad-hoc and non-systematic. In this article, we present a systematic, comprehensive, and formally founded co-verification framework for digital HW/SW systems that are modeled in SystemC. The framework is based on a formal semantics of SystemC and uses a combination of model checking and testing, whereby testing includes both the automated generation of timed inputs and automated conformance evaluation. We demonstrate its performance and its error detecting capability with two case studies, namely a packet switch and an anti-slip regulation and anti-lock braking system.

In safety-critical applications, the real-time behavior is crucial for the correctness of the overall system and must be tested thoroughly. However, the generation of test traces that cover most or all of the desired behavior of a real-time system is a difficult challenge. In this paper, we present an evolutionary algorithm that generates timed test traces, which achieve a given transition coverage. We generate these traces from a timed automata model. Our main contribution is a novel approach to encode timed test traces as individuals of an evolutionary algorithm. The major difficulty in doing so is that test traces for embedded real-time systems have to be very long. To solve this problem, we introduce the notion of blocks, which simplify long traces by cutting them into pieces. With that, we reduce the search space significantly. Furthermore, we have implemented crossover and mutation operators and a fitness function that takes time-dependent behavior implicitly into account. We show the success of our approach by experimental results from an anti-lock braking system.

The SystemC Transaction Level Modeling (TLM) standard is widely used for modeling and simulation in hardware/software co-design. However, the semantics of the TLM core interfaces is only informally defined. This makes it impossible to apply formal verification techniques to transaction level models that conform to the TLM standard. To solve this problem, we propose a formal semantics of the TLM transport mechanisms using timed automata. We achieve this by providing a set of timed automata templates that precisely capture the semantics of the TLM core interfaces. Then, we use this set to transform a given SystemC-TLM model into a semantically equivalent timed automata model. The transformation is an extension of our previously proposed transformation from SystemC into Uppaal timed automata and can be used to verify safety, liveness, and timing properties of TLM models using the Uppaal model checker. We demonstrate the applicability and performance of our approach with two case studies, namely a loosely-timed model that uses a blocking transport and an approximately-timed model that uses a 4-phase non-blocking transport.

SystemC is widely used for modeling and simulation in hardware/software co-design. However, the co-verification techniques used for SystemC designs are mostly ad-hoc and non-systematic. A particularly severe drawback is that simulation results have to be evaluated manually. In previous work, we proposed to overcome this problem by conformance testing. We presented an algorithm that uses an abstract SystemC design to compute expected output traces, which are then compared with those of a refined design to evaluate its correctness. The main disadvantage of the algorithm is that it is very expensive because it computes the output traces offline and has to cope with non-deterministic systems. Furthermore, the designer has to compare the results manually with the outputs of a design under test. In this paper, we present an approach for efficient and fully-automatic conformance evaluation of SystemC designs. To achieve this, we first present optimizations of our previously proposed algorithm for the generation of conformance tests that drastically reduce computation time and memory consumption. The main idea is to exploit the specifics of the SystemC semantics to reduce the number of semantic states that have to be kept in memory during state-space exploration. Second, we present an approach to generate SystemC test benches from a set of expected output traces. These test benches allow fully-automatic test execution and conformance evaluation. Together with our previously presented model checking framework for abstract Sys-temC designs, we yield a fully-automatic HW/SW co-verification framework for SystemC that supports the whole design process. We demonstrate the performance and error detecting capability of our approach with experimental results.