Fault Detection, Isolation, and Recovery (FDIR) components are essential for managing faults and ensuring safety and reliability in safety-critical applications. This paper presents a specification-driven approach to the automatic generation of embedded FDIR code. Our method leverages formal specifications of fault conditions and recovery procedures to synthesize fault detection and recovery mechanisms, reducing manual coding and the potential for human error. The proposed toolchain translates high-level specifications into platform-specific embedded code, while model checking can be used to validate and verify the FDIR logic. We detail the underlying architecture, the specification language, and the code generation process, highlighting the flexibility and scalability of the approach. Through a case study in the energy domain, we demonstrate the tool's ability to handle complex fault scenarios, improve development efficiency, and enhance system reliability.
Software model checking and deductive software verification have complementary strengths and weaknesses: software model checkers are more straight-forward to use, as they analyze the program without user input; but they do not yet support complicated data structures and expressive specifications. In contrast, deductive verifiers can verify expressive specifications and complex data structures modularly, but they require the user to specify the program behavior in detail, which is a time-consuming process. Due to their differing nature, the two approaches usually remain separate. However, for industrial usage, one requires both: ease of use as well as expressiveness. Therefore, we present AutoSV-Annotator, a toolchain that integrates the two approaches for C programs. The toolchain allows a user to iteratively refine the deductive annotations in a C program, calling a model checker to supplement the annotations at each iteration, guided by the already existing annotations. We show that our tool is able to annotate and prove many tasks from the SV-Benchmarks set. Our results show that the two strategies can indeed benefit from each other.
In this paper, we introduce a framework for programmable logic controller programs that combines a deductive verification approach on control flow automata with an inductive verification technique used to automatically derive loop invariants. The deductive verification is based on Hoare triples that are propagated through loop-free sections of the program using strongest postcondition and weakest precondition. Loop invariants are derived from loop pre- and postconditions with a modified version of the IC3 algorithm with predicate abstraction. While this approach is straightforward for programs with a single loop, programs with multiple loops require iterating potential loop invariants between the loops until an overall proof can be found. We demonstrate the efficacy of our approach by evaluating example programs, showing both improved performance compared to inductive verification of the complete program, and a push-button approach to deductive verification requiring – ideally – no user-supplied loop invariants.
The SAE-standardized AADL modeling language has been a significant enabler for academic and industry research on model-based development with integrated formal methods. However, several factors including industry preference for other modeling languages such as SysML, have hampered adoption of AADL and its associated formal methods technologies. The Object Management Group (OMG) is currently working on the next SysML generation (SysMLv2) that embraces several attractive characteristics of AADL and has chartered the Real-Time Embedded Safety-Critical (RTESC) working group to consider how AADL concepts, semantics, and formal specifications can be brought into the SysMLv2 ecosystem. In this paper, we report on our development of a SysMLv2 front-end for the HAMR formal-methods-integrated model-based development framework. We provide the first illustration of how the RTESC SysMLv2 libraries for AADL concepts can be used in an end-to-end tool for code generation with integrated formal methods at multiple levels. We describe how the GUMBO formal component contract language can be integrated into the SysMLv2 AADL profile to provide: (a) SMT-based integration checking at the model level, and (b) automated testing and verification of component application to architecture contracts. We present a tool architecture that enables HAMR code generation targeting the formally verified seL4 microkernel as well as other formal methods tools being applied to SysMLv2 models in the context of the Collins Aerospace DARPA PROVERS INSPECTA project.
Traditional industrial testing methods often fail to guarantee that a system behaves as expected due to the resource cost of exhaustively searching for defects. To minimize this cost, a promising alternative called robustness-guided falsification is emerging as a less exhaustive method that can handle the increasing complexity of autonomous driving systems. This approach attempts to identify counterexamples to a given system property by treating testing as an optimization problem with a robustness function to be minimized. This function quantifies how well the system satisfies a given property encoded as a logical formula, with values that indicate how close the system is to violating the property. In this paper, we apply robustness-guided falsification to a particular type of spatio-temporal logic, LTL × MS^≤ , which integrates both temporal and spatial modalities to describe system behavior across time and space. We establish a correspondence between the Boolean semantics of the “subset or equal” relation and the degrees of robustness with signed Hausdorff distances, propose a robust semantics for LTL × MS^≤ , and demonstrate how robustness-guided falsification can be applied to properties expressed in this logic. To evaluate our approach, we conducted an empirical case study in a traffic scenario. The results demonstrate the feasibility of this approach in falsifying spatio-temporal properties and support the adoption of counterexample generation for the verification of defects in realistic autonomous driving systems.
The spreading of sensor technologies has enabled railway operators to collect increasing amounts of granular data on relevant events of components and systems of railway vehicles and infrastructure, presenting unprecedented opportunities to develop predictive failure models. Our research introduces a novel methodology for synthesizing stochastic fault tree models by strategically integrating extensive diagnostic data logs, maintenance records, and domain-specific knowledge to predict component and system-level reliability dynamics. To demonstrate the potential of the approach, we apply it to the traction control unit of a fleet of regional passenger trains, showing a scalable framework for predictive failure assessment across diverse railway vehicle configurations. By leveraging existing diagnostic infrastructure without requiring additional sensor investments, our approach represents a pathway from reactive diagnostic practices to proactive maintenance strategies.
This work proposes structuring formal models using promise theory and System Theoretic Process Analysis (STPA). Promise theory enables reasoning about a system's dependency structure and information locality, a common source of complexity in cyber-physical systems. STPA, on the other hand, provides the safety constraints that a formal model must satisfy. The core idea behind the proposed approach is to prioritize modeling those parts of the system requirements that are least likely to change in later stages, hence supporting early validation through animation. We illustrate our approach by applying it to a moving block system - a prototype of a novel train protection system in the railway domain, which is currently being investigated as part of Europe's Rail Joint Undertaking.
Glitch attacks may change the behaviour of applications by inducing bit-flips in the underlying hardware. Through this, the attacker can bypass security measures of an application. Though most prevalent in systems where an attacker has physical access, recent research has shown that attacks may be performed through software alone [1, 10]. It is difficult to understand the impact of glitch attacks on a given application due to an explosion of potential execution paths. In this paper, we present a modular platform for model-checking various types of glitch attacks in RISC-V code. Developers can load a RISC-V program into a configurable virtual machine modelled in Uppaal with several attacker models available to analyse the impact of glitch attacks. The model is designed to support Uppaal Classic, SMC, and timed games with TIGA, enabling both symbolic, statistical, and game theoretical analysis. This can provide developers a valuable insight into the impact of glitch attacks on their code. Using FISSC [6], we show how all three methods complement each other.
This paper addresses the challenge of maintaining system integrity and safety during the update processes of cyber-physical systems. We propose an approach that enables updates during operation of small subsets of components, and minimizes system downtime by utilizing the inactive states of system components. The underlying contract-based design (CBD) methodology ensures that integration conditions are maintained. The approach builds upon a CBD framework that supports the specification of operating modes and formal reasoning about integration conditions, thereby providing a mechanism for managing dependencies and maintaining consistency across updates. We demonstrate the practicality of our approach with an example, highlighting how the proposed method can lead to more efficient, safe, and user-accepted updates.
Recent work on industry-capable program verification technology has emphasized the need for greater predictability in the performance of SMT-based automated verification approaches. Moreover, foundational limitations of SMT necessitate some incorporation of manual proof steps, and researchers are considering the utility of handing off some verification obligations to more powerful semi-automated interactive proof assistants. In this paper, we describe how capabilities that are usually associated with expert-level semi-automated proof assistants can be integrated synergistically in a developer-friendly code-based proof language to address many of the limitations of traditional SMT-based automated verification. Our approach enables proofs of more powerful properties to be carried out directly in a familiar programming environment rather than in a separate proof assistant tool that often utilizes low-level encodings of program semantics in annotations that are unfamiliar to industry developers. Because the proof language is implemented at the same level of abstraction as the programming language, using familiar syntax, our approach can provide easier-to-understand visualizations of rewriting/simplification steps that better align with the developer's mental model of program execution (providing a better user experience). Our approach is implemented in the open-source Logika program verifier for Slang (a safety-critical subset of Scala). We evaluate the framework on a collection of examples, including libraries for high assurance embedded system data structures developed by engineers at Collins Aerospace.
Quantitative system properties such as resilience, response times, and throughput are crucial measures in the design and operation of complex cyber-physical systems. The formal methods community has developed a variety of approaches to evaluate and optimise such properties with clear correctness and optimality guarantees. In practice, however, every application poses new challenges that require adaptations and novel combinations of the "off-the-shelf" methods we usually present in scientific papers. In this extended abstract accompanying the author's FMICS 2025 invited presentation, we use recent case studies ranging from water management for storm surge protection to routing in satellite constellations to (i) contrast the different demands on model expressiveness and tool capabilities of each application and (ii) highlight the capabilities of the Modest Toolset to solve these challenges with the varied modelling, simulation, and verification approaches it implements. In addition to these examples, we outline how quantitative verification tools can deliver the correctness and optimality guarantees we would like to see.
The increasing complexity of embedded automotive software necessitates a strong focus on safety. ISO 26262 mandates reliability in critical systems, ensuring secure and bounded memory usage, bounded execution time, and protection against division-by-zero and overflow errors. Automotive software is typically modeled in Simulink and State-flow, generating ISO 26262-compliant C code under a periodic execution paradigm. However, for data-driven applications such as automated driving, periodic execution leads to redundant computations and bus overloads, requiring manual optimization. To address these issues, we introduce GRust, a domain-specific language for automotive system modeling. GRust generates Rust implementations that enforce compiletime safety properties while optimizing execution through change propagation. Additionally, it integrates a verification wrapper of Creusot for formal property validation. This paper presents the design of GRust, its implementation, and verification capabilities, demonstrating its potential to improve both the reliability and efficiency of automotive software.
In industry, software testing is the primary method to verify and validate the functionality, performance, security, usability, and so on, of software-based systems. Test automation has gained increasing attention in industry over the last decade, following decades of intense research into test automation and model-based testing. However, designing, developing, maintaining and evolving test automation is a considerable effort. Meanwhile, AI's breakthroughs in many engineering fields are opening up new perspectives for software testing, for both manual and automated testing. This paper reviews recent research on AI augmentation in software test automation, from no automation to full automation. It also discusses new forms of testing made possible by AI. Based on this, the newly developed taxonomy, ai4st, is presented and used to classify recent research and identify open research questions.
As the complexity of software systems rises, methods for explaining their behaviour are becoming ever-more important. When a system fails, it is critical to determine which of its components are responsible for this failure. Within the verification community, one approach uses graph games and the Shapley value to ascribe a responsibility value to every state of a transition system. As this is done with respect to a specific failure, it is called backward responsibility. This paper provides tight complexity bounds for backward responsibility for reachability, Büchi and parity objectives. For Büchi objectives, a polynomial algorithm is given to determine the set of responsible states. To analyse systems that are too large for standard methods, the paper presents a novel refinement algorithm that iteratively computes responsibility and demonstrates its utility with a prototypical implementation.
The Maeslant Barrier is a storm surge barrier that protects Rotterdam and its harbour from storm surges in the North Sea. Its software control consists of three major components, one of which is BesW. BesW is responsible for all the movements of the barrier except for pushing and pulling it. In this document, we report on the complete formal specification of BesW in mCRL2. All its behaviour has been specified, including manual and testing modes. Furthermore, all fault situations have been taken into account. The formalisation allows formal verification of all behavioural properties, formulated in the modal μ-calculus, with the constraints that water levels only have a restricted number of values and not all combinations of failures of pumps and valves are allowed.
Autonomous cyber-physical systems must be able to operate safely in a wide range of complex environments. To ensure safety without limiting mitigation options, these systems require detection of safety violations by mitigation trigger deadlines. As a result of these system's complex environments, multimodal prediction is often required. For example, an autonomous vehicle (AV) operates in complex traffic scenes that result in any given vehicle having the ability to exhibit several plausible future behavior modes (e.g., stop, merge, turn, etc.); therefore, to ensure collision avoidance, an AV must be able to predict the possible multimodal behaviors of nearby vehicles. In previous work, model predictive runtime verification (MPRV) successfully detected future violations by a given deadline, but MPRV only considers a single mode of prediction (i.e., unimodal prediction). We design multimodal model predictive runtime verification (MMPRV) to extend MPRV to consider multiple modes of prediction, and we introduce Predictive Mission-Time Linear Temporal Logic (PMLTL) as an extension of MLTL to support the evaluation of probabilistic multimodal predictions. We examine the correctness and real-time feasibility of MMPRV through two AV case studies where MMPRV utilizes (1) a physics-based multimodal predictor on the F1Tenth autonomous racing vehicle and (2) current state-of-the-art deep neural network multimodal predictors trained and evaluated on the Argoverse motion forecasting dataset. We found that the ability to meet real-time requirements was a challenge for the latter, especially when targeting an embedded computing platform.
In the domain of reliability engineering and risk assessment, the development of fault tree (FT) models is pivotal for decision-making in complex systems. Traditional FT model development, relying on manual efforts and expert collaboration, is both time-consuming and error-prone. The era of Industry 4.0 introduces capabilities for automatically deriving FTs from inspection and monitoring data. This paper presents FT-MOEA-CM, an extension of the FT-MOEA algorithm for inferring FT models from failure data using multi-objective optimization. FT-MOEA-CM enhances its predecessor by integrating confusion matrix-derived metrics and incorporating parallelization and caching mechanisms. Our evaluation on six FTs from diverse application areas showcases that FT-MOEA-CM exhibits (1) enhanced robustness, (2) faster convergence and (3) better scalability than FT-MOEA, suggesting its potential in efficiently inferring larger FT models.
The proprietary State Machine Modelling Tool (SMMT), developed and maintained at Canon Production Printing, can be used to model software components using state machines and generate executable production code. We have reverse-engineered the semantics that is associated to models specified in SMMT and subsequently formalised their semantics in the mCRL2 language. Using this formalisation, we have been able to detect subtle bugs in the implementation of the SMMT tool. Moreover, our formalisation allows for verifying the models specified in SMMT before the code is generated, offering users the option to thoroughly verify their designs.
