Institute of Information Security and Dependability (KASTEL) – Application-oriented Formal Verification
Institute of Information Security and Dependability (KASTEL) – Application-oriented Formal Verification
Home

Companion Webpage for IFM'17

This is the companion webpage for our IFM'17:
Generalised Test Tables: A Practical Specification Language for Reactive Systems
Bernhard Beckert, Suhyun Cha, Mattias Ulbrich, Birgit Vogel-Heuser, and Alexander Weigl

Links

  • geteta — the backend
  • stvs — the graphical user interface

Experiment files

Tables

nuXmv commands

Apply with nuXmv -source <file.xmv> <module.smv>

[ic3, bmc, invar, itp, ltl]

Runtime

Table bmc invar itp ic3 ltl
tab1 1.75 0.50 1.15 1071.42 1.35
tab2 0.95 0.60 1.66 9038.35 1.39
tab3 0.82 0.61 1.46 0.60 0.90

ST-Code

TYPE
  OperationMode : (Learn , Active);
END_TYPE

FUNCTION SEL : INT
VAR_INPUT
        G : BOOL;
        a,b : INT;
END_VAR

     IF G THEN SEL := a;
     ELSE SEL := b; END_IF

END_FUNCTION


FUNCTION MAX : INT
VAR_INPUT
        in0 : INT;
        in1 : INT;
END_VAR

MAX := SEL(in0>=in1, in0, in1);

END_FUNCTION


(* Returns the lesser of 2 values in0 and in1
 *
 *)
FUNCTION MIN : INT
VAR_INPUT
        in0 : INT;
        in1 : INT;
END_VAR

MIN := SEL(in0<=in1, in0, in1);

END_FUNCTION


PROGRAM MinMaxWarning
VAR CONSTANT
    WAIT_BEFORE_WARNING : INT := 10; // Amount of cycles outside  before given a warning.
    WAIT_AFTER_WARNING  : INT := 5; // Amount of cycles inside, before withdraw warning.
END_VAR

VAR_INPUT
  mode     : OperationMode; // learning or active mode
  learn    : BOOL;          // True iff current signal should be learnt
  I        : INT;           // input signal
END_VAR

VAR_OUTPUT
        W       : BOOL;     // Warning flag, iff $I \not\in [lower,upper]$
        Q       : INT;      // Truncated input signal
END_VAR

VAR
        cntQuench : INT := 5;    // remaining cycles for withdraw warning
        cntHeat   : INT := 10;   // remaining cycles to signal warning

        lower : INT := 32767;    // minimal teached value
        upper : INT := -32768;   // maximal teach value
END_VAR


IF mode = OperationMode#Learn THEN // go into learning
        IF learn THEN
                lower := MIN(lower, I);
                upper := MAX(upper, I);
        END_IF
        Q := 0;
        W := FALSE;
ELSE
        IF lower <= upper THEN

        Q := MIN( upper, MAX( lower, I) );

        IF I <> Q THEN
                cntQuench := WAIT_AFTER_WARNING;
                IF cntHeat = 0 THEN
                        W := TRUE;
                ELSE
                        cntHeat := cntHeat - 1;
                END_IF
        ELSE
                cntHeat := WAIT_BEFORE_WARNING;
                IF cntQuench = 0 THEN
                        W := FALSE;
                ELSE
                        cntQuench := cntQuench - 1;
                END_IF
        END_IF

        ELSE
                W := TRUE;
                Q := 0;
        END_IF

END_IF

END_PROGRAM