Fault-Accommodating Models

We model the occurrence of a fault by an unobservable and uncontrollable event F, i. e. we extend nominal low-level events Sigma_nlo by the event F to the event set Sigma_lo = Sigma_nlo∪ {F}. A fault-accommodating model is set up in a 2-step procedure. Firstly, we model the nominal plant behaviour Ln ⊆ Sigma_pn*. Secondly we establish a model that includes the faults previous history and its impact on the plant, which we denote the plant-failure behaviour Ld ⊆ Sigma_fp*. The pair (Ln,Ld) is called a fault-accommodating model. A fault-accommodating model (Ln,Ld) is called proper if

(1) Ld ∩ Sigma_np*  ⊆  Ln
(2) (Closure(Ld)) ∩ Sigma_np*  ⊆  (Closure(Ln))

With a fault-accommodating model (Ln,Ld) we associate the fault-accommodating behaviour Lf = Ln ∪ Ld If the fault-accommodating model (Ln,Ld) is proper, then,

Lf = Ln ∪ ((Closure(Ln)) F Sigma_fp* ∩ Ld)

holds for the fault-accommodating behaviour.

Fault-Accommodating Control Reconfiguration

The problem of fault-accommodating control reconfiguration effectively is a standard control problem under partial observation. Formally, it is a tuple (Sigma_f,Lf,Ef) with a fault-accommodating plant Ln and a fault-accommodating specification Ef. We aim for a prefix-closed controller Hf such that the closed-loop system Lf || Hf

(FA1) is complete
(FA2) is non-conflicting, i. e. (Closure(Lf)) || Hf = Closure(Lf||Hf)
(FA3) is controllable w.r.t (Lf,Sigma_ucon ∪ Sigma_lof)
(FA4) satisfies the specification, i. e. Lf||Hf ⊆ Ef.

We provide a convenience function for the computation of fault-accommodating controllers.

FtcFaBehaviour

Computation of fault-accommodating behaviours.

Signature:

FtcFaBehaviour(+In+ Generator gN, +In+ Generator gD, +Out+ Generator gRes)

Detailed description:

Given a fault-accommodating model (Ln,Ld) represented by Gn and Gd, respectively, i. e. L(Gn) = Ln and L(Gd) = Ld this function evaluates

Lf = Ln ∪ ((Closure(Ln)) F Sigma_fp* ∩ Ld)

and returns an generator Gf with L(Gf) = Lf.

Example:

FtcIsProper

Test properness

Signature:

FtcIsProper(+In+ Generator gN, +In+ Generator gD, +Out+ Boolean bRes)

Detailed description:

Given a fault-accommodating model (Ln,Ld) represented by Gn and Gd, respectively, i. e. L(Gn) = Ln and L(Gd) = Ld this function checks (1) Ld ∩ Sigma_np*  ⊆  Ln and
(2) (Closure(Ld)) ∩ Sigma_np*  ⊆  (Closure(Ln)) and returns the result as a boolean value.

FtcFaController

Check properness

Signature:

FtcFaController(+In+ Generator gLfa, +In+ Generator gEfa, +In+ Alphabet aCON, +In+ Alphabet aUCON, +In+ Alphabet aHI, +Out+ Generator gC)

Detailed description:

Given are generators gLf and gEf, with Lm(gLn) = Lf and Lm(gEf) = Ef together with containers alpCON, alpUCON and alpHI that hold the controllable events Sigma_con, uncontrollable events Sigma_ucon and the high-level events Sigma_hi. This function return constructs a generator gC with Lm(gC) = Hf such that the controller Hf ensures (FA1)-(FA4) for the closed loop system Lf||Hf.

libFAUDES 2.32b --- 2024.03.08 --- with "synthesis-observer-diagnosis-iosystem-hiosys-multitasking-coordinationcontrol-timed-iodevice-simulator-luabindings"

>>