interlocked guard with rundown timer¶


suite id	`g_guard_lock`
domain	manufacturing
language	LD-graphical
difficulty	easy
validation status	validated
origin	authored
license	CC-BY-4.0

Authored from the guard-locking requirement in ISO 14119: the guard stays locked until the hazardous movement has stopped, not until the drive command drops

What is proved¶

From benchmarks/manufacturing/g_guard_lock/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`	`!(Unlocked && Motor)`	ISO 14119 guard locking: the guard is never released while the drive is energised.

Variants¶

file	expected verdict	violates	method
`program.xml`	SAFE	none	expert
`no_rundown.xml`	SAFE	none	fault-injection

Files¶

file	what it is	size	sha256
`benchmark.yml`	benchmark metadata	1.1 KB	`93ccbc44a710`
`no_rundown.xml`	ladder program, PLCopen XML	2.7 KB	`0ee531ff14bd`
`program.xml`	ladder program, PLCopen XML	4.0 KB	`3ded357e988b`
`props.yaml`	property file	0.2 KB	`1b331320d53f`
`rundown_check.props.yaml`	property file	0.5 KB	`f690a27115b8`

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.

no_rundown.xmlprogram.xml

PROGRAM g_guard_lock_no_rundown
VAR_INPUT
    OpenReq : BOOL;
    DoorClosed : BOOL;
    RunCmd : BOOL;
END_VAR

VAR_OUTPUT
    Motor : BOOL;
    Unlocked : BOOL;
END_VAR


Unlocked := OpenReq;
Motor := ((RunCmd AND DoorClosed) AND NOT OpenReq);

END_PROGRAM

PROGRAM g_guard_lock
VAR_INPUT
    OpenReq : BOOL;
    DoorClosed : BOOL;
    RunCmd : BOOL;
END_VAR

VAR_OUTPUT
    Motor : BOOL;
    Unlocked : BOOL;
END_VAR

VAR
    Rundown : TON;
END_VAR


Rundown(IN:=NOT Motor, PT:=T#30ms);
Unlocked := (Rundown.Q AND OpenReq);
Motor := ((RunCmd AND DoorClosed) AND NOT OpenReq);

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_guard_lock__no_rundown (props.yaml, expected SAFE): v8.4 SAFE
g_guard_lock__program (props.yaml, expected SAFE): v8.4 SAFE — ingestion gate failed on v8.4
guard_rundown_immediate (rundown_check.props.yaml, expected SAFE): master SAFE
guard_rundown_locked (rundown_check.props.yaml, expected VIOLATION): master VIOLATION