Safety analysis fails to propagate fault behavior within faulty component

[kfhoech]

Safety analysis fails to propagate fault behavior within the component containing the fault. That is, where a component contains a fault we expect the behavior resulting from that fault to be present in other behavior within that component. Yet, nominal (non-faulty) behavior is what is observed.

A simple, self-contained example follows:

package Example
public
    with Base_Types;

    system Valve
        features
            command_open : in data port Base_Types::Boolean;
            indicate_open : out data port Base_Types::Boolean;
        annex agree {**
            eq true_valve_is_open : bool;
            guarantee Inner_O1 "Valve Open If Commanded" :
                true_valve_is_open = command_open;
            guarantee Inner_02 "Valve Indicates Open If True Open" :
                indicate_open = true_valve_is_open;
            node stuck_false (in1 : bool, trigger : bool) returns (out1 : bool);
            let
                out1 = if trigger then false else in1;
            tel;
        **};
        annex safety {**
            fault Valve_Stuck_Closed "Valve Stuck Closed" : stuck_false {
                inputs: in1 <- true_valve_is_open;
                outputs: true_valve_is_open <- out1;
                disable: false;
                probability: 1.0e-3;
                duration: permanent;
            }
        **};
    end Valve;

    system Top_Level
        features
            input1 : in data port Base_Types::Boolean;
            output1 : out data port Base_Types::Boolean;
        annex agree {**
            guarantee Top_Level_O1 "Output Follows Input" :
                output1 = input1;
        **};
    end Top_Level;

    system implementation Top_Level.impl
        subcomponents
            valve : system Valve;
        connections
            c_in1 : port input1 -> valve.command_open;
            c_out1 : port valve.indicate_open -> output1;
        annex agree {**
            lemma L_Top_Level_01 "Valve indicates open if open" :
                valve.true_valve_is_open = valve.indicate_open;
        **};
        annex safety {**
            analyze: max 1 fault 
        **};
    end Top_Level.impl;

end Example;

In the example above, the Valve system models an actuated valve that can be commanded to open, a local variable indicating the true position of the valve, and an output indicating the position of the valve. A fault models the valve getting physically stuck closed such that it cannot respond to the command to open.

At the top level a lemma is added to measure consistency between the true position of the valve and the indicated position. Running AGREE analysis indicates that the implementation at the top level meets its contract. However, running AMASE safety analysis in the presence of faults also shows that the top level is not affected by the fault with guarantee Top_Level_O1 "Output Follows Input" being satisfied. But, the valve is stuck closed while it is commanded open. The lemma helps indicate the nature of the bug: the indicated position is computed from the nominal position of the valve, not the true position.

[kfhoech]

The Lustre code confirms that, for the given simple, self-contained valve example, the indicated position is computed from the nominal value rather than the true value. __GUARANTEE1 in node _TOP__valve uses the nominal value rather than the faulted value.

type Base_Types__Boolean = bool;
type Base_Types__Unsigned = int;
type Base_Types__Unsigned_64 = int;
type Base_Types__Unsigned_32 = int;
type Base_Types__Unsigned_16 = int;
type Base_Types__Unsigned_8 = int;
type Base_Types__Integer = int;
type Base_Types__Integer_64 = int;
type Base_Types__Integer_32 = int;
type Base_Types__Integer_16 = int;
type Base_Types__Integer_8 = int;
type Base_Types__Float = real;
type Base_Types__Float_32 = real;
type Base_Types__Float_64 = real;

node _TOP__valve(
  __ASSUME__HIST : bool;
  command_open : bool;
  inlet_pressure : real;
  time : real;
  fault__trigger__valve__fault_1 : bool;
  __fault__nominal__true_valve_is_open : bool;
  true_valve_is_open : bool;
  indicate_open : bool;
  outlet_pressure : real
) returns (
  __ASSERT : bool
);
var
  __GUARANTEE0 : bool;
  __GUARANTEE1 : bool;
  valve__fault_1__node__out1 : bool;
let
  __GUARANTEE0 = (__fault__nominal__true_valve_is_open = command_open);

  __GUARANTEE1 = (indicate_open = __fault__nominal__true_valve_is_open);

  __ASSERT = ((true_valve_is_open = (if fault__trigger__valve__fault_1 then valve__fault_1__node__out1 else __fault__nominal__true_valve_is_open)) and (__ASSUME__HIST => (__GUARANTEE1 and __GUARANTEE0)));

  valve__fault_1__node__out1 = Example__Valve__stuck_false(__fault__nominal__true_valve_is_open, fault__trigger__valve__fault_1);

  --%IVC __GUARANTEE0, __GUARANTEE1;

tel;

node main(
  valve__true_valve_is_open : bool;
  valve__indicate_open : bool;
  valve__outlet_pressure : real;
  valve____ASSUME__HIST : bool;
  output1 : bool;
  valve__command_open : bool;
  valve__inlet_pressure : real;
  valve__time : real;
  valve__fault__trigger__valve__fault_1 : bool;
  valve____fault__nominal__true_valve_is_open : bool;
  input1 : bool;
  time : real;
  __fault__event__valve__valve__fault_1 : bool;
  __fault__independently__active__valve__valve__fault_1 : bool;
  __fault__dependently__active__valve__valve__fault_1 : bool;
  __fault__global_count : int
) returns (

);
var
  __ASSUME__HIST : bool;
  __LEMMA0 : bool;
  __GUARANTEE0 : bool;
let
  --%MAIN;
  __ASSUME__HIST = (valve____ASSUME__HIST and true);

  __LEMMA0 = (valve__true_valve_is_open = valve__indicate_open);

  __GUARANTEE0 = (output1 = input1);

  assert (time = valve__time);

  assert _TOP__valve(valve____ASSUME__HIST, valve__command_open, valve__inlet_pressure, valve__time, valve__fault__trigger__valve__fault_1, valve____fault__nominal__true_valve_is_open, valve__true_valve_is_open, valve__indicate_open, valve__outlet_pressure);

  assert (valve____ASSUME__HIST = __HIST(true));

  assert (input1 = valve__command_open);

  assert (valve__indicate_open = output1);

  assert (__fault__independently__active__valve__valve__fault_1 = (__fault__event__valve__valve__fault_1 -> (__fault__event__valve__valve__fault_1 or (pre __fault__independently__active__valve__valve__fault_1))));

  assert (__fault__dependently__active__valve__valve__fault_1 = (false -> (false or (pre __fault__dependently__active__valve__valve__fault_1))));

  assert (valve__fault__trigger__valve__fault_1 = (__fault__independently__active__valve__valve__fault_1 or __fault__dependently__active__valve__valve__fault_1));

  assert (__fault__global_count = (if __fault__independently__active__valve__valve__fault_1 then 1 else 0));

  assert (__fault__global_count <= 1);

  assert true;

  assert (((time = 0.0) -> (time > (pre time))) and (true -> (time = ((pre time) + (time - (pre time))))));

  --%PROPERTY __ASSUME__HIST;
  --%PROPERTY __LEMMA0;
  --%PROPERTY __GUARANTEE0;

tel;

node Example__Valve__stuck_false(
  in1 : bool;
  trigger : bool
) returns (
  out1 : bool
);
let
  out1 = (if trigger then false else in1);

tel;

node _CLOCKED_Example__Valve__stuck_false(
  _CLK : bool;
  _INIT : bool;
  in1 : bool;
  trigger : bool
) returns (
  out1 : bool
);
let
  out1 = (if _CLK then (if trigger then false else in1) else (pre out1));

tel;

node __HIST(
  input : bool
) returns (
  hist : bool
);
let
  hist = (input -> ((pre hist) and input));

tel;

node __MinPos(
  a : real;
  b : real
) returns (
  ret : real
);
let
  ret = (if (a <= 0.0) then b else (if (b <= 0.0) then a else (if (a <= b) then a else b)));

tel;

node __Rise(
  input : bool
) returns (
  output : bool
);
let
  output = (input -> ((pre (not input)) and input));

tel;

node __Fall(
  input : bool
) returns (
  output : bool
);
let
  output = ((not input) -> ((pre input) and (not input)));

tel;