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.
