The interlock that must not fail

A safety requirement bound to ST by line range, to a test by name, and back by an rq: comment.

One name — EmergencyStop — from requirement to PLC to proof.

safety/interlock.rq

EmergencyStop {
    E-stop must drop heater enable within one scan
    valve must close before heater enables
    pressure must reach setpoint before valve opens
    implemented in ["./plc/interlock.st".EmergencyStop]
    proven by ["./plc/interlock.test.ts:drops heater within one scan"]
    @status verified
    @tags (
        iec-61131
        critical
        safety
    )
}

safety_interlock {
    guards [EmergencyStop] on every phase transition
    @status verified
}

plc/interlock.st

(* rq:["../safety/interlock.rq".EmergencyStop] *)
FUNCTION_BLOCK EmergencyStop
VAR_INPUT
    Estop_NC : BOOL;
END_VAR
VAR_OUTPUT
    HeaterEnable : BOOL;
    ValveOpen    : BOOL;
END_VAR

HeaterEnable := Estop_NC AND NOT ValveOpen;
ValveOpen    := Estop_NC AND PressureOk;
END_FUNCTION_BLOCK

plc/interlock.test.ts

test("drops heater within one scan", () => {
  const fb = new EmergencyStop();
  fb.Estop_NC = false;
  fb.cycle();
  expect(fb.HeaterEnable).toBe(false);
});

trace

EmergencyStop
  ├── ["./plc/interlock.st".EmergencyStop]
  ├── ["./plc/interlock.test.ts:drops heater within one scan"]
  └── rq: comment in ST → back to the idea