Industrial kiln door safety latch¶
| suite id | kiln_door_lockout |
| domain | building_automation |
| language | ST |
| difficulty | medium |
| validation status | candidate |
| origin | authored |
| license | CC-BY-4.0 |
Authored to probe an SLM under-enumeration failure found when generate_props.py produced only the immediate door-open interlock (P1) for this program and silently dropped the fault-latch persistence requirement (P2), despite both being stated explicitly in the source's own header comment. See ml/README.md.
What is proved¶
From benchmarks/building_automation/kiln_door_lockout/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 |
!(heater_element && door_open) |
The heating element must never be energised while the kiln door is open. |
P2 |
invariant |
!(heater_element && door_fault_latched) |
Once the door has opened during a heat cycle, the heater must stay locked out even after the door closes, until an operator resets it. |
P3 |
reachability |
reachable: heater_element && door_fault_latched |
Trigger synthesis: a witness recovers the bad state P2 forbids, so the counterexample search has a concrete target when the lockout is bypassed. |
Variants¶
| file | expected verdict | violates | method |
|---|---|---|---|
clean.st |
SAFE | none | expert |
bomb.st |
VIOLATION | P2 |
fault-injection |
Files¶
| file | what it is | size | sha256 |
|---|---|---|---|
benchmark.yml |
benchmark metadata | 1.3 KB | 2075877be975 |
bomb.st |
structured text | 1.3 KB | b5db2371c6e2 |
clean.st |
structured text | 1.1 KB | c3df804ba4bd |
props.yaml |
property file | 0.7 KB | 3a20ddd41b8c |
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.
No ESBMC run is recorded against this task yet. The lessons carry the recorded runs; see Reproducing to make your own.