Skip to content

Benchmarks

sectional door with photo-eye reversal
suite id g_door_reversal
domain building_automation
language LD-graphical
difficulty easy
validation status validated
origin authored
license CC-BY-4.0

Authored from the reversal requirement for power-operated doors in EN 13241: an obstruction sends the door back to open rather than pausing it

What is proved

From benchmarks/building_automation/g_door_reversal/props.yaml. What each kind claims, and what it becomes on either route, is on The properties we prove.

id kind claim requirement
P1 invariant !(MoveDown && Beam) The door never drives down while the photo-eye beam is broken.

Variants

file expected verdict violates method
program.xml SAFE none cross-tool-consensus
momentary.xml SAFE none fault-injection

Files

file what it is size sha256
benchmark.yml benchmark metadata 1.2 KB d7332b376e5f
momentary.xml ladder program, PLCopen XML 3.6 KB 44a7408425fd
program.xml ladder program, PLCopen XML 3.8 KB f6673a537b31
props.yaml property file 0.2 KB 61809139c726
reversal_check.props.yaml property file 0.5 KB db727e6ab299

Structured text, derived

Read off the ladder graph by runner/ld_to_st.py: every rung's contacts and coils rewritten as IEC 61131-3 assignments, in the same series/parallel logic the PLCopen XML encodes. This is a reading aid, not a second source of expected verdicts; ESBMC verifies the ladder program shown above, never this rendering.

PROGRAM g_door_reversal_momentary
VAR_INPUT
    CloseCmd : BOOL;
    OpenCmd : BOOL;
    Beam : BOOL;
    TopLimit : BOOL;
END_VAR

VAR_OUTPUT
    Reversing : BOOL;
    MoveDown : BOOL;
    MoveUp : BOOL;
END_VAR


Reversing := (Beam AND NOT TopLimit);
MoveDown := ((CloseCmd AND NOT Beam) AND NOT Reversing);
MoveUp := (OpenCmd OR Reversing);

END_PROGRAM

PROGRAM g_door_reversal
VAR_INPUT
    CloseCmd : BOOL;
    OpenCmd : BOOL;
    Beam : BOOL;
    TopLimit : BOOL;
END_VAR

VAR_OUTPUT
    Reversing : BOOL;
    MoveDown : BOOL;
    MoveUp : BOOL;
END_VAR


Reversing := ((Reversing OR Beam) AND NOT TopLimit);
MoveDown := ((CloseCmd AND NOT Beam) AND NOT Reversing);
MoveUp := (OpenCmd OR Reversing);

END_PROGRAM

Recorded runs

A task can carry two routes. ld is ESBMC's ladder front end reading the program directly. via C is the same solver reached through Beremiz and MatIEC, which is the only route that reaches ST, IL, FBD and SFC; see How ESBMC-PLC works.

  • door_reversal_latched (reversal_check.props.yaml, expected VIOLATION): master VIOLATION
  • door_reversal_momentary (reversal_check.props.yaml, expected SAFE): master SAFE
  • g_door_reversal__momentary (props.yaml, expected SAFE): v8.4 SAFE
  • g_door_reversal__program (props.yaml, expected SAFE): v8.4 SAFE