Benchmarks
Forward/reverse motor interlock
|
|
| suite id |
motor_interlock |
| domain |
motor_control |
| language |
ST |
| difficulty |
easy |
| validation status |
candidate |
| origin |
authored |
| license |
CC-BY-4.0 |
Authored by Pierre Dantas for the ESBMC-PLC-Sec curation (benchmark S2, motor interlock, secret-knock LLB), adopted into this suite
What is proved
From benchmarks/motor_control/motor_interlock/props.yaml. What each kind claims, and what it becomes on either route, is on The properties we prove.
| id |
kind |
claim |
requirement |
P1 |
mutual_exclusion |
never true together: Motor_A, Motor_B |
Forward/reverse contactors must never be energised together (contactor short / mechanical damage). |
P2 |
reachability |
reachable: Motor_A && Motor_B |
Trigger synthesis: a witness recovers the secret-knock input combination that violates the interlock. |
Variants
| file |
expected verdict |
violates |
method |
clean.st |
SAFE |
none |
cross-tool-consensus |
bomb.st |
VIOLATION |
P1 |
fault-injection |
Files
| file |
what it is |
size |
sha256 |
benchmark.yml |
benchmark metadata |
1.2 KB |
991052f93a36 |
bomb.st |
structured text |
1.5 KB |
26a146ff2920 |
clean.st |
structured text |
0.9 KB |
c4a62a2b9c00 |
props.yaml |
property file |
0.5 KB |
0f7c3a781913 |
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.
motor_interlock__bomb__viac via C (props.yaml, expected VIOLATION): master VIOLATIONmotor_interlock__clean__viac via C (props.yaml, expected SAFE): master SAFE