Formal Techniques for Safety-Critical Systems

Stability of a control system ensures that its output is under control and thus is the most important characteristic of control systems. Stability is characterized by the roots of the characteristic equation of the given control system in the complex-domain. Traditionally, paper-and-pencil proof methods and computer-based tools are used to analyze the stability of control systems. However, paper-and-pencil proof methods are error prone due to the human involvement. Whereas, computer based tools cannot model the continuous behavior in its true form due to the involvement of computer arithmetic and the associated truncation errors. Therefore, these techniques do not provide an accurate and complete analysis, which is unfortunate given the safety-critical nature of control system applications. In this paper, we propose to overcome these limitations by using higher-order-logic theorem proving for the stability analysis of control systems. For this purpose, we present a higher-order-logic based formalization of stability and the roots of the quadratic, cubic and quartic complex polynomials. The proposed formalization is based on the complex number theory of the HOL-Light theorem prover. A distinguishing feature of this work is the automatic nature of the formal stability analysis, which makes it quite useful for the control engineers working in the industry who have very little expertise about formal methods. For illustration purposes, we present the stability analysis of power converter controllers used in smart grids.

The spread of autonomous systems into safety-critical areas has increased the demand for their formal verification, not only due to stronger certification requirements but also to public uncertainty over these new technologies. However, the complex nature of such systems, for example, the intricate combination of discrete and continuous aspects, ensures that whole system verification is often infeasible. This motivates the need for novel analysis approaches that modularise the problem, allowing us to restrict our analysis to one particular aspect of the system while abstracting away from others. For instance, while verifying the real-time properties of an autonomous system we might hide the details of the internal decision-making components. In this paper we describe verification of a range of properties across distinct dimensions on a practical hybrid agent architecture. This allows us to verify the autonomous decision-making, real-time aspects, and spatial aspects of an autonomous vehicle platooning system. This modular approach also illustrates how both algorithmic and deductive verification techniques can be applied for the analysis of different system subcomponents.

Redundancy concepts are an integral part of the design of space systems. Deciding when to activate which redundancy and which component should be replaced can be a difficult task. In this paper, we refine a methodology where recovery strategies are synthesized from a model of non-deterministic dynamic fault trees. The synthesis is performed by transforming non-deterministic dynamic fault trees into Markov Automata. From the optimized scheduler, an optimal recovery strategy can then be derived and represented by a model we call Recovery Automaton. We discuss techniques on how this Recovery Automaton can be further optimized to contain fewer states and transitions and show the effectiveness of our approach on two case studies.

Recent advances in machine learning and artificial intelligence are now being applied in safety-critical autonomous systems where software defects may cause severe harm to humans and the environment. Design organizations in these domains are currently unable to provide convincing arguments that systems using complex software implemented using machine learning algorithms are safe and correct.

In this paper, we present an efficient method to extract equivalence classes from decision trees and random forests, and to formally verify that their input/output mappings comply with requirements. We implement the method in our tool VoRF (Verifier of Random Forests), and evaluate its scalability on two case studies found in the literature. We demonstrate that our method is practical for random forests trained on low-dimensional data with up to 25 decision trees, each with a tree depth of 20. Our work also demonstrates the limitations of the method with high-dimensional data and touches upon the trade-off between large number of trees and time taken for verification.

Verification of real-time systems involving hard timing constraints and concurrency is of utmost importance. Parametric timed model checking allows for formal verification in the presence of unknown timing constants or uncertainty (e. g., imprecision for periods). With the recent development of several techniques and tools to improve the efficiency of parametric timed model checking, there is a growing need for proper benchmarks to test and compare fairly these tools. We present here a benchmark library for parametric timed model checking made of benchmarks accumulated over the years. Our benchmarks include academic benchmarks, industrial case studies and examples unsolvable using existing techniques.

Formal verification provides complete and sound analysis results and has widely been advocated for the functional verification of digital circuits. Besides the functional verification, a very important aspect of digital circuit design process is their timing analysis. However, despite its importance and critical nature, timing analysis is usually performed using traditional techniques, like gate-level simulation or static timing analysis, which provide approximate results due to their in-exhaustive nature and thus may lead to an undesired functional behavior as well. To overcome these issues, we propose a generic framework to conduct the formal timing analysis using the Uppaal model checker in this paper. The first step in the proposed framework is to represent the timing characteristics of the given digital circuit using a state transition diagram in Uppaal. In this model, delays are integrated using the corresponding technology parameters and the information about timing paths is added using Quratus Prime Pro, which is used as a path extracting tool. The Uppaal timing model is then verified through TCTL properties to obtain timing related information, like maximum delay. For illustration purposes, we present the analysis of a number of real-world digital circuits, like Full Adder, 4-Bit Ripple Carry Adder, Shift Registers as well as C17, S27, S208, and S386 benchmark circuits.

The Clock Constraint Specification Language (CCSL) is a clock-based specification language for capturing causal and chronometric constraints between events in Real-Time Embedded Systems (RTESs). Due to the limitations of the existing verification approaches, CCSL lacks a full verification support for ‘unsafe CCSL specifications’ and a unified proof framework. In this paper, we propose a novel verification approach based on theorem proving and SMT-checking. We firstly build a logic called CCSL Dynamic Logic (CDL), which extends the traditional dynamic logic with ‘signals’ and ‘clock relations’ as primitives, and with synchronous execution mechanism for modelling RTESs. Then we propose a sound and relatively complete proof system for CDL to provide the verification support. We show how CDL can be used to capture RTES and verify CCSL specifications by analyzing a simple case study.

Statechart modelling notations, with so-called ‘run to completion’ semantics and simulation tools for validation, are popular with engineers for designing systems. However, they do not support formal refinement and they lack formal static verification methods and tools. For example, properties concerning the synchronisation between different parts of a system may be difficult to verify for all scenarios, and impossible to verify at an abstract level before the full details of sub-states have been added. , on the other hand, is based on refinement from an initial abstraction and is designed to make formal verification by automatic theorem provers feasible, restricting instantiation and testing to a validation role. In this paper, we introduce a notion of refinement, similar to that of , into a ‘run to completion’ Statechart modelling notation, and leverage ’s tool support for proof. We describe the pitfalls in translating ‘run to completion’ models into refinements and suggest a solution. We illustrate the approach using our prototype translation tools and show by example, how a synchronisation property between parallel Statecharts can be automatically proven at an intermediate refinement level.

We present an abstraction refinement-based technique for checking safety properties of software. The technique employs predicate abstraction and SAT-based 3-valued bounded model checking. In contrast to classical refinement techniques where a single state space model is iteratively explored and refined with predicates, our approach is as follows: We use a coarsely-abstracted model of the full state space where we check for abstract witness paths for the property of interest. For each detected abstract witness we construct a partial model whose state space is restricted to refinements of the witness only. On the partial models we check whether the witness is real or spurious. We eliminate spurious witnesses in the full model via constraints, which do not increase the state space complexity. Our technique terminates when a real witness in a partial model can be detected, or no more witnesses in the full model exist. The approach enables verification with a reduced state space complexity.

This work proposes a new graph grammar formalism, that introduces non-terminal symbols to triple graph grammars (TGG) and shows how to apply it to solving the model transformation problem. Our proposed formalism seems to suit code generation from models well, outperforms the standard TGG in the grammar size in one evaluated case and is able to express one transformation that we could not express with TGG. We claim, that such advantages make a formal specification written in our formalism easier to validate and less error-prone, what befits safety-critical systems specially well.