emergency stop with monitored manual reset¶


suite id	`g_estop_reset`
domain	motor_control
language	LD-graphical
difficulty	easy
validation status	validated
origin	authored
license	CC-BY-4.0

Authored from the reset requirement in ISO 13850 and ISO 13849-1: the safety function is restored by a separate manual action, never by releasing the actuator

What is proved¶

From benchmarks/motor_control/g_estop_reset/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`	`!(Run && EStop)`	ISO 13850 stop function: the drive is never energised while the emergency stop is actuated.

Variants¶

file	expected verdict	violates	method
`program.xml`	SAFE	none	cross-tool-consensus
`auto_reset.xml`	SAFE	none	fault-injection

Files¶

file	what it is	size	sha256
`auto_reset.xml`	ladder program, PLCopen XML	2.6 KB	`b8ca85ab016f`
`benchmark.yml`	benchmark metadata	1.2 KB	`38b23f76d6d9`
`program.xml`	ladder program, PLCopen XML	4.2 KB	`f5c1c2055de6`
`props.yaml`	property file	0.2 KB	`1ce16a3f5a05`
`restart_check.props.yaml`	property file	0.5 KB	`c0b53659bed5`

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.

auto_reset.xmlprogram.xml

PROGRAM g_estop_reset_auto
VAR_INPUT
    EStop : BOOL;
    Reset : BOOL;
    Start : BOOL;
END_VAR

VAR_OUTPUT
    Safe : BOOL;
    Run : BOOL;
END_VAR


Safe := NOT EStop;
Run := ((Safe AND Start) AND NOT EStop);

END_PROGRAM

PROGRAM g_estop_reset
VAR_INPUT
    EStop : BOOL;
    Reset : BOOL;
    Start : BOOL;
END_VAR

VAR_OUTPUT
    ResetEdge : BOOL;
    Safe : BOOL;
    Run : BOOL;
    Reset_prev : BOOL;
END_VAR


ResetEdge := (Reset_prev AND NOT Reset);
Safe := ((Safe OR ResetEdge) AND NOT EStop);
Run := ((Safe AND Start) AND NOT EStop);
Reset_prev := Reset;

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.

estop_restart_auto (restart_check.props.yaml, expected SAFE): master SAFE
estop_restart_monitored (restart_check.props.yaml, expected VIOLATION): master VIOLATION
g_estop_reset__auto_reset (props.yaml, expected SAFE): v8.4 SAFE
g_estop_reset__program (props.yaml, expected SAFE): v8.4 SAFE