Skip to content

Benchmarks

burner purge, light-off and lockout
suite id g_burner_purge
domain hvac
language LD-graphical
difficulty easy
validation status validated
origin authored
license CC-BY-4.0

Authored from the light-off order in EN 298: purge, prove flame, then admit main gas, with a lockout that needs a manual reset

What is proved

From benchmarks/hvac/g_burner_purge/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 !MainValve || (PurgeDone && FlameProven) EN 298 light-off order: the main gas valve opens only after the purge has completed and the flame is proven.

Variants

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

Files

file what it is size sha256
benchmark.yml benchmark metadata 1.2 KB bafe499ed037
lockout_check.props.yaml property file 0.4 KB d95e72df20cc
program.xml ladder program, PLCopen XML 4.8 KB 8d5a0314b1d6
props.yaml property file 0.2 KB 0d8c0bb4baa6
self_clearing.xml ladder program, PLCopen XML 4.6 KB e9618b8c237c

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_burner_purge
VAR_INPUT
    CallForHeat : BOOL;
    PurgeDone : BOOL;
    FlameProven : BOOL;
    FlameFail : BOOL;
    ResetBtn : BOOL;
END_VAR

VAR_OUTPUT
    Fan : BOOL;
    Lockout : BOOL;
    Pilot : BOOL;
    MainValve : BOOL;
END_VAR


Fan := CallForHeat;
Lockout := ((Lockout OR FlameFail) AND NOT ResetBtn);
Pilot := ((CallForHeat AND PurgeDone) AND NOT Lockout);
MainValve := (((CallForHeat AND PurgeDone) AND FlameProven) AND NOT Lockout);

END_PROGRAM

PROGRAM g_burner_purge_self_clearing
VAR_INPUT
    CallForHeat : BOOL;
    PurgeDone : BOOL;
    FlameProven : BOOL;
    FlameFail : BOOL;
    ResetBtn : BOOL;
END_VAR

VAR_OUTPUT
    Fan : BOOL;
    Lockout : BOOL;
    Pilot : BOOL;
    MainValve : BOOL;
END_VAR


Fan := CallForHeat;
Lockout := (FlameFail AND NOT ResetBtn);
Pilot := ((CallForHeat AND PurgeDone) AND NOT Lockout);
MainValve := (((CallForHeat AND PurgeDone) AND FlameProven) AND NOT Lockout);

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.

  • burner_lockout_latched (lockout_check.props.yaml, expected VIOLATION): master VIOLATION
  • burner_lockout_selfclearing (lockout_check.props.yaml, expected SAFE): master SAFE
  • g_burner_purge__program (props.yaml, expected SAFE): v8.4 SAFE
  • g_burner_purge__self_clearing (props.yaml, expected SAFE): v8.4 SAFE