Sift-Out Modular Redundancy

Sift-Out Modular Redundancy

Alternatywny model TMR, wyjścia są przesyłane do porównywacza/wykrywacza, który uznaje moduł za wadliwy w momencie, gdy jego wyjście jest inne niż wszystkie pozostałe wyjścia modułów. Następnie odpowiedzi modułów wraz z informacją o uszkodzonych modułach są przekazywane do "zbieracza", który jako wyjście ma wartość taka, jak jeden z modułów, który jeszcze nigdy nie zawiódł.

Rys.6 - Diagram modelu SMR

Rys.7 - diagram agenta Det

Kod w VP:

(* sift-out modular redundancy (3 moduły) *)

const I = {1,2,3} (* indeksy modułu *)
const V = {0,1} (* wartości wejścia/wyjścia modułu *)
const Bool = {true,false}
const IV = prod(I,V)
const BV = prod(Bool,V)
const N = 3 (* ilość modułów *)
const T0 = <<0,0,0>> (* N-tka 0 *)

label in(V),out(V) (* wejście/wyjście systemu *)
label mi_I(V),mo_I(V) (* wejście/wyjście modułu *)
label do_I(BV) (* wyjście wykrywacza *)
label pass_I(IV) (* port między-wykrywacza *)
label fail_I,detect_I (* uszkodzenie modułu, wykrywanie błędów *)
label ack

(* rozdzielający 1-3 *)
agent S = in(x).sum(i:I,'mi_i(x).sum(j:diff(I,{i}),'mi_j(x).sum(k:diff(I,{i,j}),'mi_k(x).ack.S)))

(* moduł *)
agent M(i:I) = mi_i(x).('mo_i(x).M(i) + fail_i.sum(y:diff(V,{x}),'mo_i(y).M(i)))

(* moduł doskonały, indeksowane wejście i wyjście *)
agent MP(i:I) = M(i)\{fail_i}

(* moduł doskonały, nie indeksowane wejście i wyjście *)
agent MPU = in(x).'out(x).MPU

(* porównywacz i wykrywacz *)
agent D(i:I) = mo_i(x).P(i,x,<<i,x>>,true)

agent P(i:I,x:V,jy:IV,b:Bool) = 'pass_((i mod N)+1)(jy).pass_i(kz).
              if i = kz#1 then P'(i,x,b)
              else P(i,x,kz,b and not x=(kz#2))

agent P'(i:I,x:V,b:Bool) =
              if b then detect_i.P''(i,x,b)
              else P''(i,x,b)

agent P''(i:I,x:V,b:Bool) = 'do_i(<<b,x>>).D(i)

(* moduł akceptujący, gdy ma wiadomość *)
agent D'(i:I) = mo_i(x).Q(i,x,<<i,x>>,true)

agent Q(i:I,x:V,jy:IV,b:Bool) = pass_i(kz).'pass_((i mod N)+1)(jy).
              if i = kz#1 then Q'(i,x,b)
              else Q(i,x,kz,b and not x=(kz#2))

agent Q'(i:I,x:V,b:Bool) =
              if b then detect_i.Q''(i,x,b)
              else Q''(i,x,b)

agent Q''(i:I,x:V,b:Bool) = 'do_i(<<b,x>>).D'(i)

(* złożony wykrywacz *)
agent Det = (D'(1) | D(2) | D(3))\{pass}

(* zbieracz *)
agent C = C'(<<false,false,false>>)

agent C'(B:prod(Bool,Bool,Bool)) = sum(i:I,do_i(ax).sum(j:diff(I,{i}),do_j(by).sum(k:diff(I,{i,j}),do_k(cz).
C''(update(update(update(B,i,B#i or ax#1),j,B#j or by#1),k,B#k or cz#1),update(update(update(T0,i,ax#2),j,by#2),k,cz#2)))))

agent C''(B:prod(Bool,Bool,Bool),X:prod(V,V,V)) = sum(i:I,if not B#i then 'out(X#i).'ack.C'(B))

(* sift-out modular redundancy *)
agent SMR = (S|M(1)|M(2)|M(3)|Det|C)\{mi,mo,do,ack}

(* wersja używana do pokazania tolerowanych błędów, ukryte wykrywanie *)
agent Hide1 = 'fail_2.Hide1 + 'fail_3.Hide1 + 'detect_2.Hide1 + 'detect_3.Hide1
agent SMR1 = ((S|M(1)|MP(2)|MP(3)|Det|C)\{mi,mo,do,ack}|Hide1)\{fail,detect}

(* wersja używana do pokazania wykrywania błędów, ukryte wejście i wyjście *)
agent Hide2 = sum(x:V,'in(x).Hide2) + out(x).Hide2
agent SMR2 = ((S|M(1)|MP(2)|MP(3)|Det|C)\{mi,mo,do,ack}|Hide2)\{in,out}

(* cykliczne błędy/detekcje *)
agent Cycler = fail_1.detect_1.Cycler

eq (SMR1, MP); True

eq (SMR2, Cycler); True