Stop-on-equal comparison cycle (graphical LD)¶


suite id	`g_stop_eq`
domain	motor_control
language	LD-graphical
difficulty	easy
validation status	candidate
origin	plc-ld-dataset
license	GPL-3.0

PLC-LD-dataset, github.com/UniboSecurityResearch/PLC-LD-dataset (Iacobelli et al., ICPS 2024, doi:10.1109/ICPS59941.2024.10639995); legitimate/lstop_eq.xml

What is proved¶

From benchmarks/motor_control/g_stop_eq/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`	`!(STOP && CYCLE_ON)`	STOP input must force the cycle off (safety interlock).

Variants¶

file	expected verdict	violates	method
`lstop_eq.xml`	SAFE	none	expert

Files¶

file	what it is	size	sha256
`NOTES.md`	notes	0.2 KB	`b566db2beb36`
`benchmark.yml`	benchmark metadata	0.7 KB	`d2af40286749`
`lstop_eq.xml`	ladder program, PLCopen XML	20.2 KB	`d94f8a9adcdd`
`props.yaml`	property file	0.2 KB	`2cfc67d17b11`

Structured text, derived¶

Read off the ladder graph by runner/ld_to_st.py: every rung's contacts and coils rewritten as IEC 61131-3 assignments, in the same series/parallel logic the PLCopen XML encodes. This is a reading aid, not a second source of expected verdicts; ESBMC verifies the ladder program shown above, never this rendering.

lstop_eq.xml

PROGRAM program0
VAR_INPUT
    TLB2 : INT;
    TLB1 : INT;
    STOP : BOOL;
    START : BOOL;
    IN1 : INT;
    VALUE : INT;
END_VAR

VAR_OUTPUT
    MV1 : BOOL;
    MV2 : BOOL;
    CYCLE_ON : BOOL;
END_VAR

VAR
    valves_handler0 : valves_handler;
    stop_cycle0 : stop_cycle;
END_VAR


valves_handler0(EN:=CYCLE_ON, IN1:=VALUE, IN_TLB1:=TLB1, IN_TLB2:=TLB2);
stop_cycle0(EN:=NOT CYCLE_ON);
CYCLE_ON := ((CYCLE_ON OR (IN1 = 1)) AND NOT STOP);
MV1 := valves_handler0.OUT_MV1;  (* 2 writers to MV1: scan order decides which value survives *)
MV2 := valves_handler0.OUT_MV2;  (* 2 writers to MV2: scan order decides which value survives *)
MV1 := stop_cycle0.OUT_MV1;  (* 2 writers to MV1: scan order decides which value survives *)
MV2 := stop_cycle0.OUT_MV2;  (* 2 writers to MV2: scan order decides which value survives *)

END_PROGRAM

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.

g_stop_eq__lstop_eq (props.yaml, expected SAFE): v8.4 SAFE