Benchmarks
interlocked guard with rundown timer (ST twin)
|
|
| suite id |
st_guard_lock |
| domain |
manufacturing |
| language |
ST |
| difficulty |
easy |
| validation status |
candidate |
| origin |
authored |
| license |
CC-BY-4.0 |
| syntax pair of |
g_guard_lock |
Structured Text rendering of g_guard_lock, for cross-language comparison of the same safety function
What is proved
From benchmarks/manufacturing/st_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 |
guard_lock.st |
SAFE |
none |
expert |
Files
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.
st_guard_lock__guard_lock__viac via C (props.yaml, expected SAFE): master SAFE