bus coupler auto-changeover (graphical LD)¶


suite id	`g_bus_coupler_changeover`
domain	power_substation
language	LD-graphical
difficulty	medium
validation status	validated
origin	authored
license	CC-BY-4.0

Authored for this suite, modeling a two-incomer/bus-coupler auto-changeover scheme

What is proved¶

From benchmarks/power_substation/g_bus_coupler_changeover/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`	`!(incomer_a && incomer_b && coupler)`	The coupler may parallel at most one healthy incomer onto the affected section; all three breakers must never be closed together.

Variants¶

file	expected verdict	violates	method
`clean.xml`	SAFE	none	expert
`bomb.xml`	VIOLATION	`P1`	fault-injection

Files¶

file	what it is	size	sha256
`benchmark.yml`	benchmark metadata	1.1 KB	`132709776daa`
`bomb.xml`	ladder program, PLCopen XML	3.4 KB	`3866017ee7c8`
`clean.xml`	ladder program, PLCopen XML	3.0 KB	`80413e1774d1`
`props.yaml`	property file	0.3 KB	`108d7a0fe7e8`

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.

bomb.xmlclean.xml

PROGRAM g_bus_coupler_changeover_bomb
VAR_INPUT
    incomer_a_healthy : BOOL;
    incomer_b_healthy : BOOL;
    maint : BOOL;
END_VAR

VAR_OUTPUT
    incomer_a : BOOL;
    incomer_b : BOOL;
    coupler : BOOL;
END_VAR


incomer_a := incomer_a_healthy;
incomer_b := incomer_b_healthy;
coupler := ((NOT incomer_a_healthy AND incomer_b_healthy) OR (maint AND incomer_a_healthy));

END_PROGRAM

PROGRAM g_bus_coupler_changeover_clean
VAR_INPUT
    incomer_a_healthy : BOOL;
    incomer_b_healthy : BOOL;
    maint : BOOL;
END_VAR

VAR_OUTPUT
    incomer_a : BOOL;
    incomer_b : BOOL;
    coupler : BOOL;
END_VAR


incomer_a := incomer_a_healthy;
incomer_b := incomer_b_healthy;
coupler := (NOT incomer_a_healthy AND incomer_b_healthy);

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.

g_bus_coupler_changeover__bomb (props.yaml, expected VIOLATION): v8.4 VIOLATION
g_bus_coupler_changeover__clean (props.yaml, expected SAFE): v8.4 SAFE