A car that moves with its door open¶

This machine appears twice in the catalog: once as a ladder rung and once as a sequential function chart. The same hazard is built into both, and the two bombs are not built the same way. That difference is the lesson.

The machine¶

An elevator car with a powered door and a drive. The door opens on request when the car is level with a floor, and the drive runs when a move is commanded.

A car that travels with its door open exposes the running shaft to whoever is standing in the doorway. It is the failure every lift interlock exists to prevent, and it is the reason a lift has a door contact in series with the drive circuit rather than a signal somewhere in software.

benchmarks/elevator/g_elevator_door/props.yaml

format_version: "0.1"
properties:
  - id: P1
    kind: mutual_exclusion
    variables: [door_open, drive]
    justification: "The door must never be open while the car is driving."

As a ladder rung¶

door_open := NOT move_req AND open_req AND at_floor
drive     := move_req

file	what it is	size	sha256
`clean.xml`	ladder program, PLCopen XML	2.7 KB	`c106fb097ac9`
`bomb.xml`	ladder program, PLCopen XML	3.2 KB	`3a7c07acb28c`
`sfc_elevator_door_clean.xml`	ladder program, PLCopen XML	5.8 KB	`cf95eef742f7`
`sfc_elevator_door_bomb.xml`	ladder program, PLCopen XML	5.9 KB	`4096b3df387c`

Recorded 2026-09-04T23:40:44Z. Every build ran the same command.

cp benchmarks/elevator/g_elevator_door/clean.xml benchmarks/elevator/g_elevator_door/clean.ld
esbmc benchmarks/elevator/g_elevator_door/clean.ld --ld-props benchmarks/elevator/g_elevator_door/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

Recorded 2026-09-04T23:40:44Z.

v8.4

cp benchmarks/elevator/g_elevator_door/clean.xml benchmarks/elevator/g_elevator_door/clean.ld
esbmc benchmarks/elevator/g_elevator_door/clean.ld --ld-props benchmarks/elevator/g_elevator_door/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

build	ESBMC	verdict	expected	outcome	ingestion gate	cpu
v8.4	8.4.0	`SAFE`	`SAFE`	correct	pass	0.017 s

v8.4 found its solution by the inductive step (k = 2).

What the front end encoded. The scan body as the solver receives it, branch guards kept. An assignment-only view hides the guards and makes a guarded accumulator read as a constant.

v8.4

     1: IF !1 THEN GOTO 2
        ASSIGN open_req=NONDET(_Bool);
        ASSIGN move_req=NONDET(_Bool);
        ASSIGN at_floor=NONDET(_Bool);
        ASSIGN maint=NONDET(_Bool);
        ASSIGN drive=1 && move_req;
        ASSIGN door_open=1 && !move_req && open_req && at_floor;
        GOTO 1
     2:

The bombed rung is the branch you have seen three times now, and it puts the car in motion with the door open:

Recorded 2026-09-04T23:40:44Z. Every build ran the same command.

cp benchmarks/elevator/g_elevator_door/bomb.xml benchmarks/elevator/g_elevator_door/bomb.ld
esbmc benchmarks/elevator/g_elevator_door/bomb.ld --ld-props benchmarks/elevator/g_elevator_door/props.yaml --incremental-bmc --unwind 20 --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

Recorded 2026-09-04T23:40:44Z.

v8.4

cp benchmarks/elevator/g_elevator_door/bomb.xml benchmarks/elevator/g_elevator_door/bomb.ld
esbmc benchmarks/elevator/g_elevator_door/bomb.ld --ld-props benchmarks/elevator/g_elevator_door/props.yaml --incremental-bmc --unwind 20 --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

build	ESBMC	verdict	expected	outcome	ingestion gate	cpu
v8.4	8.4.0	`VIOLATION`	`VIOLATION`	correct	pass	0.013 s

What the front end encoded. The scan body as the solver receives it, branch guards kept. An assignment-only view hides the guards and makes a guarded accumulator read as a constant.

v8.4

     1: IF !1 THEN GOTO 2
        ASSIGN open_req=NONDET(_Bool);
        ASSIGN move_req=NONDET(_Bool);
        ASSIGN at_floor=NONDET(_Bool);
        ASSIGN maint=NONDET(_Bool);
        ASSIGN drive=1 && move_req;
        ASSIGN door_open=1 && !move_req && open_req && at_floor;
        ASSIGN door_open=1 && move_req && maint && open_req && at_floor;
        GOTO 1
     2:

Counterexample. ESBMC's own output. A trace long enough to need it is elided in the middle, and the omission is marked and counted where it happens.

v8.4

State 1  thread 0
----------------------------------------------------
  open_req = 1

State 2  thread 0
----------------------------------------------------
  move_req = 1

State 3  thread 0
----------------------------------------------------
  at_floor = 1

State 4  thread 0
----------------------------------------------------
  maint = 1

State 5  thread 0
----------------------------------------------------
  drive = 1

State 6  thread 0
----------------------------------------------------
  door_open = 1

State 7 file benchmarks/elevator/g_elevator_door/bomb.ld thread 0
----------------------------------------------------
Violated property:
  file benchmarks/elevator/g_elevator_door/bomb.ld
  P1
  !(door_open && drive)

open_req = 1   move_req = 1   at_floor = 1   maint = 1   ->   door_open = 1   and   drive = 1

Both builds catch it. Nothing new so far.

As a sequential function chart¶

The same lift, written as the sequence it really is:

Four steps, four transitions, two actions. door_open is held while the chart sits in Opening, moving while it sits in Moving, and since a chart is in one step at a time the hazard is prevented by the structure rather than by a contact.

Now the bombed chart. Here is the entire difference between the two files:

-<action localId="40" qualifier="N"><reference name="door_open" /></action>
+<action localId="40" qualifier="S"><reference name="door_open" /></action>

One letter. N holds the action while its step is active and releases it on the way out. S stores it: door_open is set on entry to Opening and no later step ever clears it, so the car reaches Moving with the door still commanded open.

Nothing was added. The steps are the same steps, in the same order, with the same actions attached to the same places. Print the two charts side by side and they are identical drawings.

What the verifier says about the chart¶

Recorded 2026-09-04T23:40:45Z. Every build ran the same command.

cp benchmarks/elevator/sfc_elevator_door/clean.xml benchmarks/elevator/sfc_elevator_door/clean.ld
esbmc benchmarks/elevator/sfc_elevator_door/clean.ld --ld-props benchmarks/elevator/sfc_elevator_door/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

Recorded 2026-09-04T23:40:45Z.

v8.4

cp benchmarks/elevator/sfc_elevator_door/clean.xml benchmarks/elevator/sfc_elevator_door/clean.ld
esbmc benchmarks/elevator/sfc_elevator_door/clean.ld --ld-props benchmarks/elevator/sfc_elevator_door/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

build	ESBMC	verdict	expected	outcome	ingestion gate	cpu
v8.4	8.4.0	`SAFE`	`SAFE`	correct	fail	0.014 s

v8.4 found its solution by the inductive step (k = 2).

What the front end encoded. The scan body as the solver receives it, branch guards kept. An assignment-only view hides the guards and makes a guarded accumulator read as a constant.

v8.4

     1: IF !1 THEN GOTO 2
        ASSIGN call=NONDET(_Bool);
        ASSIGN dwell_done=NONDET(_Bool);
        ASSIGN door_closed=NONDET(_Bool);
        ASSIGN at_floor=NONDET(_Bool);
        GOTO 1
     2:

Recorded 2026-09-04T23:40:46Z. Every build ran the same command.

cp benchmarks/elevator/sfc_elevator_door/bomb.xml benchmarks/elevator/sfc_elevator_door/bomb.ld
esbmc benchmarks/elevator/sfc_elevator_door/bomb.ld --ld-props benchmarks/elevator/sfc_elevator_door/props.yaml --incremental-bmc --unwind 20 --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

Recorded 2026-09-04T23:40:46Z.

v8.4

cp benchmarks/elevator/sfc_elevator_door/bomb.xml benchmarks/elevator/sfc_elevator_door/bomb.ld
esbmc benchmarks/elevator/sfc_elevator_door/bomb.ld --ld-props benchmarks/elevator/sfc_elevator_door/props.yaml --incremental-bmc --unwind 20 --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

build	ESBMC	verdict	expected	outcome	ingestion gate	cpu
v8.4	8.4.0	`unknown`	`VIOLATION`	unknown	fail	0.076 s

What the front end encoded. The scan body as the solver receives it, branch guards kept. An assignment-only view hides the guards and makes a guarded accumulator read as a constant.

v8.4

     1: IF !1 THEN GOTO 2
        ASSIGN call=NONDET(_Bool);
        ASSIGN dwell_done=NONDET(_Bool);
        ASSIGN door_closed=NONDET(_Bool);
        ASSIGN at_floor=NONDET(_Bool);
        GOTO 1
     2:

Read the ingestion gate. It fails on both variants, because ESBMC's front end discards an <SFC> body without a diagnostic. The clean chart reports SAFE having verified nothing, and the bombed chart reports unknown.

So the same hazard, in the same catalog, written by the same author: caught in ladder, invisible in SFC. Not because the SFC bomb is subtler, but because the tool never read the file. That is the coverage story from How ESBMC-PLC works arriving where it costs something.

Why the qualifier is a good place to hide¶

An attack does not have to add anything. Review by shape and you are looking for extra branches, extra contacts, extra steps, and there are none here. The difference is an attribute on an element that is supposed to be there, using a feature of the standard that is entirely legitimate, and stored actions are common enough in real charts that seeing one raises nothing.

The same trick exists in ladder: flip a negated attribute on a contact and the drawing barely changes. --ld-fault-injection plants exactly that class of defect, negating contact polarities and degrading Set and Reset coils to plain output coils, so you can check your properties would notice.

What to take from this¶

Two lessons, and they pull in opposite directions.

A benchmark suite has to carry the notations its tools cannot read. If this catalog held only the ladder version, the SFC bomb would not exist to be missed, and the gap in coverage would look like an absence of problems rather than an absence of evidence.

And a property is worth more than a review. Nothing about reading either chart finds the S. The requirement !(moving && door_open) finds it the moment a tool can read the body at all, which for this notation is a job still waiting to be done.