Observers and safety properties

5 Observers and safety properties

Translating a Stateflow chart into Lustre allows the application of tools such as the model-checker Lesar or the abstract interpretation tool Nbac to be applied to the chart. The sf2lus translator supports this process with several features.

5.1 Observers in Lustre

Firstly, we can pass an expression to the translator and it will build an observer for that expression:

% sf2lus -names -states_visible SetReset_r13.mdl -o SetReset_r13.lus \
  -observe "((sOn and not sOff) or (sOff and not sOn))"

This will result in the following node being appended to the Lustre output:

-- observer for expr: ((sOn and not sOff) or (sOff and not sOn))
node verif_2_1(Set, Reset: event) returns(prop: bool);
var x: int;
let
  x = sf_2(Set, Reset);
  prop = ((sOn and not sOff) or (sOff and not sOn));
tel

The name of the observer node is verif_<CID>_<index> where <CID> is the chart id as before and <index> is a unique index for the observer (verif becomes verify under -long_names). This can then be passed to Lesar for checking:

% lesar SetReset_r13.lus verif_2_1 -v -diag
--Pollux Version 2.1
start normalisation ... done
start minimal network generation ..... done (90 -> 64 nodes)
building bdds ... 6 (on 6)   

computing relevant statevars ... done (3 on 3)
DONE =>     3 states     5 transitions              

=>total bdd memory : 59 nodes (~ 5.99 K)
TRUE PROPERTY

In fact the process can be automated somewhat since the translator automatically looks for an observer file when a model file is translated. This file has the same name as the model file but with .mdl replaced by .obs. The format of this file is simply one observer per line with blank lines and Lustre-style comments (starting with --) ignored. This behaviour can be switched off using the -no_observers option.

We can build complex safety properties using this mechanism but it is a bit inconvenient having to develop the observers in Lustre.

5.2 Observers in Stateflow

We can, however, build observers in Stateflow by providing parallel states at the toplevel which have one boolean free value.

Figure 5: A Stateflow chart with an observer node

Figure 5 shows a Stateflow chart (SetResetV.mdl) with an observer implemented in Stateflow. If a toplevel node called ``Observer'' exists in the chart with a boolean output called ``prop'' (or ``property'' with -long_names) then a Lustre observer node for prop is automatically appended to the translated output. We can thus use all of Stateflow's action language to build observers which means that the designer does not have to learn Lustre and that the observed property is visible in the Stateflow chart.

5.3 Types of observers

We can write observers for application-specific safety properties in either Lustre or Stateflow. The EMSOFT'04 paper [4] describes a simple safety observer and how it was used to debug a Stateflow model (taxi_verif_sf2.mdl). However, we can also use these observers to help translate imperative features such as event broadcasting or parallel state confluence.

5.3.1 Parallel state confluence

Figure 6: An observer for parallel state confluence

Consider the chart in Figure 6 (Parallel6V.mdl). This contains two copies of a subchart with parallel states which are identical apart from the order in which the parallel states are visited. The observer simply compares, state by state, the two parallel machines. If we translate the chart into Lustre and run Lesar on it:

% sf2lus Parallel6V.mdl -o Parallel6V.lus -names -states_visible
% lesar Parallel6V.lus verif_2_1
--Pollux Version 2.1

TRUE PROPERTY

We get a TRUE property showing that the two versions of the subchart are indeed equivalent and thus their parallel states are confluent.

The above chart implemented the observer in Stateflow but we may also wish to keep two copies of the chart and compare them externally. The problem here is that the namespaces of the two translated charts would be identical so sf2lus allows the visible node names to be prefixed, for example:

% sf2lus Parallel6_12.mdl -o Parallel6_12A.lus -prefix A -names -states_visible
% sf2lus Parallel6_21.mdl -o Parallel6_21B.lus -prefix B -names -states_visible

This allows a comparative observer to be built in Lustre, as follows:

include "Parallel6_12A.lus";
include "Parallel6_21B.lus";

node verif(S1, R1, S2, R2: bool) returns(prop: bool)
AsgN1, AsB, AsA, AsgN2, AsD, AsC, 
BsgN1, BsB, BsA, BsgN2, BsD, BsC: bool;
let
  AsC, AsD, AsA, AsB, AsgN2, AsgN1 = Asf_2 (S1, R1, S2, R2);
  BsA, BsB, BsC, BsD, BsgN1, BsgN2 = Bsf_2 (S1, R1, S2, R2);
  prop = AsgN1 = BsgN1 and AsgN2 = BsgN2 and
         AsA = BsA and AsB = BsB and
         AsC = BsC and AsD = BsD;
tel

This simply includes both versions of the chart with alternate parallel state order and compares the outputs. The strange ordering of the output variables is due to the fact that inputs and outputs are indexed according to the id numbers of the data, events, states and junctions. Stateflow orders these according to its internal priorities.

In theory, these observers could be built automatically but for now they have to be built by hand.

5.3.2 Event stack depth

When the event stack mechanism is used there is an implicit assumption that the Stateflow model is bounded in its event stack. To support this the translator can add an additional output err (or error in -long_names format) which is set to true if there is an attempt to broadcast an event at the lowest level of the event stack. Consider again the chart in Figure 2. If we translate the chart with an event stack of 1 and run Lesar on the output:

% sf2lus Events3.mdl -o Events3.lus -errstate -ess 1
% lesar Events3.lus verif_2_1
--Pollux Version 2.1

FALSE PROPERTY

We get a FALSE property because we tried to broadcast the F output event while processing the E event at level 1 of the event stack. For this chart we actually need an event stack of 2:

% sf2lus Events3.mdl -o Events3.lus -errstate -ess 2
% lesar Events3.lus verif_2_1
--Pollux Version 2.1

TRUE PROPERTY

Beware, however, that the -errstate variable is not set if you do not define an event stack, a false positive will result. The sf2lus translator assumes that you know the chart is confluent if you do not use an event stack.

5.3.3 Automatic observers

The observer in Section 5.2 is a simple internal consistency check upon the state variables. In fact, we can automate the generation of such an observer by scanning the chart and building an expression for each subgraph. For exclusive (OR) states there should be either no active state if the subgraph is inactive or one and only one active state if the subgraph is active. For parallel (AND) states there should be no active state if the subgraph is inactive or all the states should be active simultaneously. The -consistency option triggers the generation of just such an observer (called consistency_<CID>).

For example, the model in Figure 3 generates the following observer:

-- Observer for state consistency
node consistency_2(E: event) returns(prop: bool);
var y, x, z: real; sB, sC, sA, sE, sD, sgTop2, sgTop1: bool;
let
  y, x, z, sB, sC, sA, sE, sD, sgTop2, sgTop1 = sf_2(E);
  prop =
    ((sgTop1 and sgTop2) and
     (if sgTop1
      then ((sD and ((not sE) and (not sA))) or
            (((not sD) and (sE and (not sA))) or
            ((not sD) and ((not sE) and sA))))
      else (not (sD or (sE or sA))) and
      if sgTop2 then ((sC and (not sB)) or ((not sC) and sB))
      else (not (sC or sB))));
tel

Observers for junction entry counters are discussed in Section 4.2.