Chemical dosing overdose lockout with lamp and pump-inhibit readouts¶


suite id	`chemical_feed_fault_lockout`
domain	water_treatment
language	LD-textual
difficulty	easy
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 fans out to two independent readouts, where the safety property is about the trigger, not the readouts' mutual relationship.

What is proved¶

From benchmarks/water_treatment/chemical_feed_fault_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`	`overdose_sensor -> !dose_pump_run`	An overdose condition must stop the dosing pump in the same scan it is sensed; the property is grounded in the sensor trigger, not in dose_pump_run's relationship to the unrelated fault_lamp readout.
`P2`	`reachability`	reachable: `overdose_sensor && dose_pump_run`	Witness: overdose_sensor=1, dose_req=1 reaches dose_pump_run=1 in bomb, because dose_fault no longer latches on the overdose sensor at all.

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	`21a5ff248127`
`bomb.ld`	ladder program, textual DSL	0.4 KB	`a457104f64e0`
`clean.ld`	ladder program, textual DSL	0.2 KB	`2dde4ae8384a`
`props.yaml`	property file	0.6 KB	`25d90822746a`

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.

chemical_feed_fault_lockout__bomb (props.yaml, expected VIOLATION): v8.4 error — ingestion gate failed on v8.4
chemical_feed_fault_lockout__clean (props.yaml, expected SAFE): v8.4 VIOLATION