Protection trip cascading through a lockout latch to breaker close¶


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

Authored for the esbmc-plc-benchmark-suite to close a training gap found by ml/scripts/build_task_slice.py: a latch that feeds a second latch, where the safety property must trace back through both hops to the original trigger.

What is proved¶

From benchmarks/power_substation/protection_lockout_cascade/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`	`protection_trip -> !breaker_close`	A protection trip must block breaker closure through both latch stages (trip_latch then lockout_latch); the property is grounded in the original trigger two hops upstream, not in the trip_latch/lockout_latch pair's own mutual wiring.
`P2`	`reachability`	reachable: `protection_trip && breaker_close`	Witness: protection_trip=1, close_req=1 reaches breaker_close=1 in bomb, because lockout_latch stopped reading trip_latch even though trip_latch itself still latches correctly.

Variants¶

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

Files¶

file	what it is	size	sha256
`benchmark.yml`	benchmark metadata	1.2 KB	`14d7023b7c6e`
`bomb.ld`	ladder program, textual DSL	0.5 KB	`b19d2b08e39e`
`clean.ld`	ladder program, textual DSL	0.3 KB	`40dc8e0693ee`
`props.yaml`	property file	0.6 KB	`bdfa70b6b563`

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.

protection_lockout_cascade__bomb (props.yaml, expected VIOLATION): v8.4 VIOLATION
protection_lockout_cascade__clean (props.yaml, expected SAFE): v8.4 VIOLATION