Start/stop cycle controller (graphical LD)¶


suite id	`g_start_cycle`
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/lstart_cycle.xml

What is proved¶

From benchmarks/motor_control/g_start_cycle/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)`	Classic seal-in safety: pressing STOP must release the holding circuit so the motor/cycle cannot remain energized.
`P2`	`invariant`	`!(START && STOP && CYCLE_ON)`	Simultaneous START and STOP should not leave the cycle active (STOP has priority).

Variants¶

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

Files¶

file	what it is	size	sha256
`NOTES.md`	notes	0.2 KB	`829ae5311d1e`
`benchmark.yml`	benchmark metadata	0.8 KB	`90158f1e0561`
`lstart_cycle.xml`	ladder program, PLCopen XML	19.8 KB	`9469074398fd`
`props.yaml`	property file	0.4 KB	`006467d32e0f`

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.

lstart_cycle.xml

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

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

VAR
    start_cycle0 : start_cycle;
    valves_handler0 : valves_handler;
    stop_cycle0 : stop_cycle;
END_VAR


start_cycle0(EN:=TRUE, IN1:=CYCLE_ON);
valves_handler0(EN:=start_cycle0.OUT, IN1:=VALUE, IN_TLB1:=TLB1, IN_TLB2:=TLB2);
stop_cycle0(EN:=NOT CYCLE_ON);
CYCLE_ON := ((START OR CYCLE_ON) 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_start_cycle__lstart_cycle (props.yaml, expected SAFE): v8.4 SAFE