Analysis of diagnostic models using formal methods

Formal study of diagnostic properties (diagnosability, identifiability, etc.) in dynamic systems (discrete, continuous, hybrid).


The implementation of monitors, diagnostics or fault protection systems is severely compromised if some requirements are not met by the system at the design time. These requirements are expressed in terms of diagnosability, identifiability and reconfigurability/repairability. These properties make it possible to know in advance which faults or states the diagnostician will be able to discriminate with the instrumentation in place, and which faults the controller will be able to compensate for with the actuators provided. In addition, these properties make it possible to identify the set of additional sensors and actuators that are needed to achieve the required degree of diagnosability and/or reconfigurability/repairability, and even to provide self-healing capabilities in autonomous systems.

The research activities carried out by the DISCO team cover the diagnosability of continuous systems, with a focus on uncertain non-linear systems, discrete-event systems and hybrid systems. A unified definition of diagnosability, independent of system type, has been established on the basis of the notion of signature. Identifiability is also studied as an essential property when parameter estimation methods are used for diagnosis. Bridges with diagnosability are under study. Particular attention is paid to distributed systems, often made up of a network of components. Local properties are studied in order to deduce global diagnosability, enabling the automatic deployment of a protocol between local diagnostic agents whose resulting diagnostic capacity is optimal.


CUS

FOCUS

Functional diagnosability and links with identifiability

In contrast to the classic definition, functional diagnosability exploits the temporal properties of analytical redundancy relationships linked to the various faults, known as functional signatures. Functional diagnosability is closely linked to the notion of identifiability, which guarantees that the parameters of a model can be unambiguously deduced from measurements of system outputs. This link provides a sufficient condition for testing the functional diagnosability of a system. Functional diagnosability has been extended to the assembly framework and linked to assembly identifiability. The impact of ensemblistic identifiability on the properties of solutions obtained by parameter estimation was analyzed.

Diagnosability and fault pattern diagnosis

A diagnosability analysis is an a priori analysis performed on the system to ensure that when the system is in operation, if a fault occurs, a diagnostic function will be able to determine it with certainty and in a finite time. Diagnosability analysis in discrete-event systems is based on the search for a critical pair, i.e. two evolutions of the system with the same observable trace as the observed evolution, such that the fault is present in one of these two evolutions and absent in the other. Diagnosis is formally characterized by the notion of pattern matching and posed as an attainability problem solved by model checking. The search for critical pairs is based on the construction of a twin-plant and a cycle search within the twin-plant, formulated as an attainability problem in Linear Temporal Logic.

Diagnosability of hybrid systems

The method determines a first discrete abstraction of the continuous dynamics of a hybrid automaton and checks the diagnosability of the resulting automaton by standard methods for discrete-event systems. These check whether there is a counterexample, i.e. a critical pair of trajectories with the same observable projection, one with fault and the other normal. If no counterexample is found, then the abstraction is diagnosable, which confers the property on the initial hybrid system. Otherwise, the counter-example is analyzed and guides the current abstraction to refinement. This method thus constructs an incomplete hierarchy of abstractions for hybrid system diagnosability.