Priostack · Engineering Blog · 21 August 2026 · 9 min read

Safety by Construction: Deterministic Control at the Edge

Deep diveSkopinEngineering

Most control code out in the field is written the way most code is written: a loop, a pile of if statements, some flags to remember what happened last time, and a comment that says do not remove this check. It works. It usually keeps working. And then one day two conditions line up that nobody thought to test together, a flag is stale, and a pump runs while a valve is closed.

The honest response to that is not "test harder". You cannot test your way to a guarantee about a state you never imagined. The interesting response is to change what kind of thing the control logic is - so that the dangerous state is not something you check for and reject at runtime, but something the system has no way to represent in the first place. That is what running edge control as a Petri net buys you, and it is the reason a device running Skopin does not execute your control logic as a script.

This piece is about that shift: from "we test that it cannot happen" to "it cannot happen". It is specific to how Qubit and Skopin work, and it is honest about where the guarantee ends.

1. The trouble with ad-hoc control

Imperative control code has a specific failure mode, and it is worth naming precisely. The safety of the system lives in the gaps between the statements - in the order they run, in which flags are set when, in whether every path that reaches the "start the pump" line also passed through the "valve is open" check. None of that is written down as a property. It is emergent from the control flow, and control flow is exactly the thing that grows tangled as a device picks up features.

You end up defending an invariant - "the pump never runs against a closed valve" - by scattering checks near every place the pump might start. Miss one path, or add a new one later, and the invariant is quietly false. The code still compiles. The tests you have still pass, because they exercise the paths you thought of. The property was never a property; it was a habit.

A Petri net inverts this. The logic is not a sequence of statements that might preserve an invariant. It is a structure of places and transitions where the invariant is a fact about the structure. You do not check it on every tick. It holds because the graph cannot express its violation.

2. The scan cycle: one clean tick

On a control device, Skopin runs a fast, repeating scan cycle - on the order of 120 milliseconds. Each cycle is the same disciplined shape, and the discipline is the point:

  every ~120 ms:

  1. SENSE     read every input at once      -> a snapshot
  2. EVALUATE  which transitions are enabled  (pure, no I/O)
  3. FIRE      move tokens for enabled ones    -> next marking
  4. ACT       drive outputs from new marking
                     |
                     +--> repeat, from a known state

Two things matter here. First, inputs are sampled once, at the top of the cycle, into a single snapshot. The whole evaluation then reasons about one consistent picture of the world. There is no reading a sensor, doing some work, and reading it again to get a value that has since changed underneath you - the class of bug where a decision is made on two different versions of reality.

Second, evaluation is pure. Deciding which transitions may fire touches no hardware and has no side effects. It is a function from the current marking plus the input snapshot to the next marking. Only after that decision is settled does the cycle drive outputs. Sense, decide, act - never interleaved, never racing.

3. Sensor conditions as read-only guards

When a technology-layer Node in an ArchiMate model is a real device running Skopin, its sensors do not become variables the control logic can assign to. They become read-only guards on transitions.

A guard is a condition that must hold for a transition to be allowed to fire. "Valve open" is a guard. "Tank below high-level" is a guard. The control logic can read these; it cannot forge them. There is no path where code sets valveOpen = true to get past a check - the guard reflects a live sensor reading from the current snapshot, and nothing in the model can write to it. The physical world is an input, never a variable.

This sounds like a small distinction and it is a large one. In imperative code the guard and the thing it guards are both mutable state, and the whole game is keeping them honest with respect to each other. As a read-only guard on a transition, the sensor condition is structurally on one side of the line. It gates behaviour; behaviour cannot gate it back.

• read_only guards - the transition observes a condition it cannot alter.
• the snapshot is the source of truth - every guard in one cycle reads the same consistent picture.
• no ambient writes - the logic drives declared outputs and nothing else; it has no back door to the inputs.

4. Unsafe states, made unreachable

Here is the core move. In a Petri net, the state of the system is its marking - where the tokens sit. An interlock is expressed as a structural constraint on markings: certain combinations of tokens simply cannot co-occur, because the transitions that would produce them do not exist, or their guards make them permanently disabled.

Take the pump and the valve. Model it so that the token representing "pump running" can only be produced by a transition guarded on "valve open", and so that "valve closing" consumes the precondition the pump needs. Now the marking "pump running AND valve closed" is not a state you check for and reject. It is a state with no incoming transition. It is unreachable. Nothing in the model can put the tokens there.

  (valve open) ---guard---> [ start pump ] ---> (pump running)
                                                      |
  (valve closing) --------> [ stop pump ] <----------+
                              consumes the running token
                              before the valve can shut

  the marking { pump running, valve closed }
  has NO transition that produces it -> unreachable by construction

This is safety by construction, and it is a property of Petri-net semantics rather than a feature Skopin bolts on. The unsafe interlock states are not made invalid; they are made non-existent. There is a difference between a door you lock and a wall where a door was never cut. Runtime checks are locks - and a lock can be bypassed by the one path that forgot to consult it. Structural unreachability is a wall.

5. "We test it can't" versus "it can't"

This is the sentence the whole article turns on, so let it stand on its own.

"We test that it cannot happen" is a statement about your test suite. It says: across the scenarios we thought to run, the bad state did not appear. It is evidence, and evidence is bounded by imagination. The states you never pictured are exactly the ones the tests never covered, and those are the ones that hurt you at 3 a.m.

"It cannot happen" is a statement about the structure. It says: the bad marking has no path that reaches it, and here is the analysis of the net that shows why. It does not depend on which scenarios anyone dreamed up. It holds for the scenarios nobody dreamed up too.

Neither approach makes a sensor honest or a wire unbroken - we will get to that. But within the logic, the second one is a different category of claim. You move from a probabilistic argument about coverage to a deductive one about structure.

6. The same model, on every surface

The reason this is practical rather than academic is that the net is not a separate artifact you draw once and then reimplement in device firmware. It is the model that runs. Qubit is the single engine under the Priostack app, the API, and the edge device, and it runs BPMN 2.0, DMN 1.3 and CMMN 1.1 natively - BPMN executed with Petri-net semantics. The same model means the same thing on every surface because the same engine interprets it everywhere.

So the process you designed - reviewed in an ArchiMate model, expressed as BPMN, its decisions in DMN - is not "translated for the controller". Priostack deploys it to the device over Skopin's own protocol; Skopin runs those models and policies out in the field and reports the device's real state back. The behaviour you reasoned about on the whiteboard is the behaviour that fires every 120 ms on the board in the cabinet. There is no second implementation to drift out of sync with the first.

7. Priostack, Skopin, Reflex

The division of labour is worth stating plainly, because each layer earns a different kind of trust.

• Priostack orchestrates. It holds the canonical process, decision and case state, and it deploys models to devices.
• Skopin executes at the edge. It is the Linux edge OS that runs the app's models and policies on the device itself, scan cycle and all, and reports real state back. Because the models run locally, the control loop does not depend on a network round trip to decide whether the pump may start.
• Reflex anchors it in the physical world. The reference edge hardware - a small Linux board with Wi-Fi, 4G, eSIM, microSD, IEEE 802.15.4, and expansion for Z-Wave, XBee and LoRa - is where sensors and actuators actually connect.

An ArchiMate technology Node stops being a diagram box and becomes a device you can deploy to and get truthful state from. The structure you modelled and the metal in the field are the same subject, described once.

8. Where the guarantee ends

Structural safety is a strong claim about the logic, and it is easy to oversell into a claim about the whole system. It is not that. Being specific about the boundary is the honest part.

So the guarantee is: given honest inputs, the control logic will not command an unsafe combination, because that combination is not a state the net can hold. Everything outside that box - sensor integrity, actuator health, the physical process - still needs redundancy, plausibility checks, and hardware interlocks in the traditional sense. Structural unreachability removes one large and slippery class of failure, the logic-level one that ad-hoc code is worst at. It does not remove the world's ability to break.

The other honest limit is scope. This works because control interlocks are the kind of thing Petri nets express well - discrete states, guarded transitions, forbidden combinations. Not everything a device does fits that shape, and what a model cannot express, the surrounding app provides as a permissioned native feature, granted for a stated purpose with an expiry and enforced when it is invoked. The net is the right tool for the interlock. It is not asked to be the right tool for everything.

Conclusion

The move is small to state and large in consequence. Stop writing edge control as a script that checks an invariant on every tick, and start expressing it as a structure where the invariant is a property of the shape. Sample the world once per cycle into a clean snapshot. Let sensor conditions be read-only guards the logic can read but never forge. Build the net so the unsafe markings have no incoming transition, and verify that by reachability analysis before the device is ever powered.

What you get is not a better test suite. It is a different kind of sentence you are allowed to say. Not "in everything we tried, it did not happen", but "it cannot happen, and here is the structure that shows why" - bounded, honestly, by the truthfulness of the sensors and the health of the metal. That boundary is real, and naming it is part of the guarantee, not a footnote to it.