Fail-Safe Motor Latch¶


suite id	`g_failsafe_motor_latch`
domain	motor_control
language	LD-graphical
difficulty	easy
validation status	validated
origin	lessons-electric-circuits
license	Design Science License

Lessons In Electric Circuits, Volume IV - Digital, Chapter 6 (Fail-safe design), by Tony R. Kuphaldt

What is proved¶

From benchmarks/motor_control/g_failsafe_motor_latch/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`	`THERMAL_OVERLOAD_NC \|\| !MOTOR_RUN`	Fire Hazard: The motor coil must instantly de-energize if the hardware thermal overload relay physically trips (opening the NC circuit).

Variants¶

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

Files¶

file	what it is	size	sha256
`NOTES.md`	notes	1.4 KB	`7454246fc95e`
`benchmark.yml`	benchmark metadata	0.8 KB	`60e87b1bfdeb`
`failsafe_motor_latch.xml`	ladder program, PLCopen XML	3.0 KB	`3d16843f5bb5`
`props.yaml`	property file	0.3 KB	`c3fb22b09d1e`

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.

failsafe_motor_latch.xml

PROGRAM main
VAR
    START : BOOL;
    THERMAL_OVERLOAD_NC : BOOL;
    STOP_NC : BOOL;
    MOTOR_RUN : BOOL;
END_VAR


MOTOR_RUN := (((START OR MOTOR_RUN) AND THERMAL_OVERLOAD_NC) AND STOP_NC);

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_failsafe_motor_latch__failsafe_motor_latch (props.yaml, expected SAFE): v8.4 SAFE