Modular Diagnosis.

In practice, it is common that technical systems are composed of a number of components that are synchronised via shared events. For the purpose of diagnoses, the literature proposes decentralized ([D3]) and modular ([D6]) diagnoser architectures that aim for diagnosis on a per component basis. The diagnosis plug-in currently supports the latter case of modular diagnosis. Here, only local observations in each individual component may be utilized to identify failures w.r.t. a local specification. Information from the remaining components is only used implicitely via the synchronisation of shared events and the component behaviour, but not explicitly by directly observing events.

IsModularDiagnosable

Tests for modular diagnosability w.r.t. local specifications for each subsystem.

Signature:

IsModularDiagnosable(+In+ SystemVector GVArg, +In+ GeneratorVector KVArg, +Out+ Boolean BRes)

Detailed description:

This function realizes the modular diagnosability verification based on the plant in the form of n components Gi,i = 1,...,n and one specification Ki for each plant.

Although the test essentially verifies the diagnosability of each component specification Ki,i = 1,...,n with respect to the overall plant G = G1 || ... || Gn and the observation of the respective component, our implementation does not require to evaluate the overall plant G. Instead, we compute appropriate system abstractions as described in Tobias Barthel's diploma thesis.

Parameter Conditions:

All generators must be deterministic. Alphabets of component models and specifications must match.

Example

This example illustrates the usage of IsModularDiagnosable.

Consider the system G consisting of the two components G1 and G2 with two corresponding local specifications K1 and K2. The only observable event in the example is the event alpha, and a failure happens in the component G2 if the event b occurs.

Component G1 Component G2
 
Local specification K1 Local specification K2
 
Abstraction \hat{G}_1 Abstraction \hat{G}_2

Looking at G1 and K1 only, faulty strings that contain the event b cannot be distinguished from non-faulty strings since the only observable event alpha can occur in both cases. However, in conjunction with G2, the observable event alpha can only happen after a faulty string. Hence, IsModularDiagnosable determines that modular diagnosability is fulfilled (note that there is no faulty behavior specified by K2 anyway). Furthermore, it is the case that the overall plant G = G1||G2 need not be computed. It is sufficient to compute the abstracted plant \hat{G} = \hat{G}_1||\hat{G}_2 to verify modualr diagnosability.

In order to demonstrate a case, where modular diagnosability fails, we consider the next example that generates a failure if the event b occurs in G1. In contrast to the previous example, it holds that the observation in G1 would be sufficient to resolve the failure as soon as the observable event alpha occurs more than twice. However, the composition with G2 enables only one occurrence of alpha. Hence, the result of IsModularDiagnosable is false

Component G1 Local specification K1
Component G2 Local specification K2

ModularDiagnoser

Compute diagnoser for subsystems with local specifications.

Signature:

ModularDiagnoser(+In+ SystemVector GVArg, +In+ GeneratorVector KVArg, +Out+ GeneratorVector DVArg, +Out+ Boolean BRes)

Detailed description:

If modular diagnosability is fulfilled for a system with multiple components and local specifications, a modular diagnoser can be computed for each component in order to detect failures while following the respective local observation of the system behavior. The computation of such modular diagnoser is implemented in the function ModularDiagnoser.

Parameter Conditions:

All generators must be deterministic. Alphabets of component models and specifications must match.

Example

The following figure shows the modular diagnosers for the first example discussed above. In the case of the component G2, a failure is detected as soon as the observable event alpha occurs. No failure occurs in the second component G2 which is also reflected by the corresponding diagnoser.

Diagnoser for G1
Diagnoser for G2

libFAUDES 2.32b --- 2024.03.01 --- with "synthesis-observer-observability-diagnosis-hiosys-iosystem-multitasking-coordinationcontrol-timed-simulator-iodevice-luabindings-hybrid-example-pybindings"