Combining techniques of formal verification and probabilistic assessment for determining the degree of confidence in safety critical digital systems


Context

Digital systems are everywhere: they control critical processes and transactions fundamental for the functioning of the economy and the society of industrialized countries. It is therefore paramount that these systems can be trusted to satisfy essential safety and security properties. There exists a large body of research work in both control theory and computer science for building up theories and mathematically rigorous techniques that underpin establishing system properties. These include formal verification methods for proving that digital systems are free from critical errors, as well as probabilistic methods for evaluating the degree of confidence that can be placed in these systems. Unfortunately, these existing methods can rarely be combined for the analysis of industrial systems. In particular, the models are usually written at different levels of abstraction, although in both approaches Boolean operators play an important role for expressing safety and security properties. The analysis is difficult mainly because of the complexity of digital systems of industrial relevance, due to the high number of physical and software components that interact strongly, but also to the complexity of the algorithms, including different voting algorithms necessary to ensure fault tolerance.

 

Structural properties of a system often give rise to monotonicity of the Boolean functions that underlie probabilistic evaluation. Researchers at CRAN have developed methods that exploit this property, relying on the minimal tie-set[1] and extending the analysis by propagation of their effect along the state graph of the system, which can be seen as an ordering induced by a Hasse diagram [1,2]. Satisfiability problems arise in this context in order to analyze the state graph, and researchers at LORIA develop efficient techniques and tools for solving these problems.

 

Objectives of the PhD thesis

The PhD thesis aims at a convergence of the works mentioned above concerning probabilistic evaluation and satisfiability solving for symbolic verification. Concretely, we suggest adapting the latter techniques for use in the context of the structural analysis of dysfunctional models used for the probabilistic evaluation of safety and security properties of critical digital systems and therefore for determining the degree of trust that can be placed in these systems. As described above, satisfiability problems arise naturally within a methodological approach that exploits the monotonicity properties of state graphs and thus leads to a demonstrated improvement with respect to standard techniques used in this context.

 

Proposed work and expected results

Preliminary safety analyses usually give rise to specifications in different formats (such as OpenPSA [3,4], Figaro [5] etc.) that represent fault trees, reliability diagrams or Boolean driven Markov processes [6,7]. These specifications can mathematically be represented as one or several Boolean functions. Based on this representation, the work proposed in this thesis consists in the use of formal verification, and in particular SMT (satisfiability modulo theories [8]) techniques, in order to determine the minimal tie-sets of a coherent system[2]. In the case of non-coherent systems, it should be possible to compute the set of terminal tie-sets as well as residual cut-sets,[3] based on the formal verification of safety properties. Starting from the sets obtained in this way, the ordered state graph can be generated, and the degree of trust in the system will be determined based on a probabilistic assessment of the graph [1,2]. In this way, an overall joint methodology is obtained in which both the formal verification of safety properties and the evaluation of trust levels are possible for a given system.

 

Moreover, the specifications that result from preliminary safety analyses usually reflect all possible failures (detected and undetected dangerous failures as well as failures that are not safety critical), and the corresponding Boolean functions rather express information on the reliability or availability of the system. In a safety case, it will be appropriate to simplify the model and only consider the failures that affect the considered safety properties in the sense that the model should reflect the failures that lead to a violation of these properties. Formal verification techniques will lead to a decomposition of the system into sub-systems, at least some of which will still respect their safety requirements. It will then be possible to generate ordered sub-graphs of states that are simplified with respect to the sub-systems, leading to a simpler probabilistic assessment of the degree of trust in the sub-systems. A method must then be developed for evaluating the trust in the overall system based on the results of prior verification and/or quantitative evaluation of the sub-systems.

 

The extension of this approach to components whose behavior is no longer represented by a Boolean variable but exhibits multiple values leads to a multi-dimensional state graph. Such a representation will be able to represent different degrees of degraded safety during the lifetime of the system and can be the basis of a dynamic analysis of the degree of trust that can be placed in the system.

The conceptual work developed during the PhD thesis will lead to an improvement of methods for evaluating the trust in safety-critical digital systems (Safety Instrumented Systems, SIS, systems that must comply with the IEC 61508 standard or its specific variants to application fields: process industries, nuclear power plants, automotive or railway, …) that are the main applicative target of this research work. These systems exhibit a behavior that can not just be understood as a simple cause-effect relationship. Indeed, modern SIS used for ensuring the safety and security of critical processes (e.g., nuclear plants for the production of electric energy, rail-bound or airborne transport systems) are complex digital systems with a high level of redundancy for guarding against component failures, and their interactions lead to novel types of risks. Our work will establish safety properties of the software controlling these systems, as well as of the hardware platforms on which the software is deployed. These platforms consist of distributed entities that communicate over computer networks and that may have to execute in real time. The results will be validated jointly with our industrial partners (such as EDF, RATP, Total, and ClearSy).

 

Since they have to ensure the safety and security of critical industrial processes, SIS act as a firewall that must guarantee the security and the trust in networks. Moreover, SIS include mechanisms that ensure the consistency of the data stored in a database but also control the access rights to this data in a decentralized system with several administrators, in order to ensure that users can have sufficiently high levels of trust in the use of the data. In this sense, the developments planned during this PhD thesis are not just relevant for the 4th axis of the Impact project concerning the safety of industrial-critical digital systems, but should also be useful for other axes of the project in order to formally verify or quantitatively assess different trust levels.

[1] A tie-set is a subset of components (respectively, of the Boolean variables modeling these components) such that if all these components operate correctly (and hence the corresponding Boolean variables are all true) and all other components are failed (and hence the corresponding Boolean variables are all false), the system represented by the overall function works correctly.

[2] A system is called coherent if: (i) its structure function is monotonic, (ii) it operates correctly when all its components work, and (iii) it fails when all its components fail. A system is non-coherent if there exists a subset of components such that the system works when all these components work, but the system fails when one of the other failed components is repaired or such that the system is failed when a given subset of components are failed and a new failure of the other working components brings back the system in working state. In other words, a non-coherent system can transit from a failed state to a working state by the failure of a component, or transit from a working state to a failed state by the repair of a component.

[3] A cut-set is a subset of components (or the Boolean variables that represent them) such that the failure of precisely these components (all variables equal false) leads to the system failure (the overall structure reliability function of the system evaluates to false).

 

Supervision

Thesis advisors: Nicolae Brinzei and Stephan Merz

Research laboratories: CRAN (CNRS UL) and LORIA (CNRS, Inria, UL)

PhD school: IAEM Lorraine Lorraine Graduate School

Contact :

nicolae.brinzei@univ-lorraine.fr, phone: +33 (0)3 83 59 56 36
stephan.merz@loria.fr, phone: +33 (0)3 54 95 84 78

How to apply

In order to prepare a PhD thesis within the Lorraine Université d’Excellence Program, the interested candidate should consult the PhD topics offered in each social and economic challenges.
These PhD thesis topics are proposed by faculty members or researchers accredited to supervise research.

Candidate application period: according to graduate school schedule (visit each topic)
Each candidate may submit an application on up to three separate research topics.

Application analysis period by each graduate school
The graduate school reviews the applicants for a doctoral contract in the relevant disciplines. They check the level of supervision for each supervisor and the situation of trained doctors. Each candidate will meet the laboratory director, supervisor and a representative from the graduate school. This interview is to identify the candidate’s motivations and suitability as a candidate for the PhD project proposed by the supervisor. A recommendation will be made to the graduate school. This will summarize the strengths and/or weaknesses of the application.

PhD grants will include monthly income for the PhD student (roughly 1700 € for research only, complement can be provided for teaching missions)) and environment for research in the research unit.

Please be aware that in order to offer a variety of subjects, more positions are posted here than available funding. The LUE executive committee will make the final choice on the granted funding (up to 12 positions), based on the recommendations by the doctoral schools.