Verification: formal checks, tests, faults and logs

How archec checks that the model is right: the state machines and contracts it proves, the requirements that cannot hold together, the tests with faults, their coverage, and the real system's logs read against the model.

Formal checks: state machines and contracts#

The linter reads each state machine as a graph (a definition's with the states and transitions of the ones it extends, as Arche gets it):

code	what it finds
`unreachable-state`	a state no path reaches from the initial state. Entering a composite starts in its `pseudo initial` child (else its first; one per `region`), and a transition that never fires leads nowhere. `goto("X")` in the code reaches X.
`deadlock-state`	a reachable state with no way out, nor from a state around it, that is not `pseudo final`. It is a warning when the machine has a final state, and a hint when it has none, since a latched fault that only a reset leaves is often meant. A state every state falls into (`* -> Fault`) is a safe state. A component whose code calls `goto(…)` is not checked.
`dead-transition`	a trigger that is a message no input port of the component receives (`receives`, its handlers, its interfaces' `messages`; a port that says none takes anything), or a guard that is `false`
`shadowed-transition`	a transition that an earlier one beats every time: same state, same trigger, and the earlier one has no guard
`nondeterministic` (hint)	two guarded transitions from one state on one trigger whose guards may both hold. `else`, `g` / `not g`, distinct values and disjoint ranges (`x < 0` / `x >= 0`) count as exclusive.

A guard is read only when it is a plain comparison; one written in words is left alone.

A contract says what a component assumes of what it receives and guarantees of what it sends:

component BrakeEcu {
  in cmd: can-fd receives BRAKE_CMD
  out status: can-fd sends BRAKE_STATUS
  contract {
    assume cmd.force in 0..1000N
    assume cmd.mode != 2
    guarantee status.applied within 20ms after cmd
  }
}

A clause names a port's message field (cmd.force, or cmd.BRAKE_CMD.force) or a variable, compared with in lo..hi, ==, !=, <, <=, >, >=, or bare (status.applied, not fault). Clauses can be joined by and, opened with always or eventually, and closed with within 20ms [after port]. An interface or a port type can hold a contract too. Its clauses name the message or the field, and they hold on every port that takes part in it.

At each link a.p -> b.q, what a guarantees on p must imply what b assumes on q:

Ranges and equalities on the same field. A guarantee in 0..1500N against an assumption in 0..1000N is a contract-unmet warning that quotes both sides.
Units. Time units are converted. Others are not: N against kN is a contract-unknown hint, and N against ms is unmet.
Deadlines. A guarantee within 20ms meets an assumption within 50ms. When both name an after event, a link must join the two ports.

An assumption with nothing guaranteed on its field is contract-unknown, and so is a clause archec cannot read (an or, a call). Arche has no place for contracts, so they stay in the model. archec sysml writes them as a requirement of assume constraints and require constraints.

Requirements that cannot hold together#

archec verify --conflicts looks for requirements no implementation can satisfy together, as NASA's FRET does, with nothing to install. It reads the formal properties and the EARS sentences over each part's states. At each tick the environment chooses which message each part receives; the implementation then puts each part in any of its states (the machine's transitions are one implementation, not a limit), starting from its initial one. When no choice of states survives every input, the requirements conflict:

✗ conflict R1, R2 cannot hold together [req-conflict]
    at 10ms, when brakes receives watchdog, every state the parts can be in breaks R1 or R2
         0  brakes in Idle
      10ms  brakes receives watchdog → whatever the parts do:
              brakes in Idle     breaks R2
              brakes in Braking  breaks R2
              brakes in Holding  breaks R2
              brakes in Fault    breaks R1
    main.arche:31 R1: never brakes in Fault
    main.arche:32 R2: if brakes receives watchdog then brakes shall be in Fault

Each conflict is minimal: leave out any one requirement and the rest can hold. It is a safety game on a finite graph (the parts' states and, per requirement, the earliest deadline it awaits), solved exactly. What is bounded: time is counted in ticks, the deadlines' common divisor (made coarser past 16 ticks per deadline, each rounded up; --tick sets it); eventually and leads to with no within are read as within --horizon ticks (8); a response that sends a message is not read.

archec verify --meaning [REQ…] shows what a property says, on two timelines, one where it holds and one where it fails (the specification from archec doc --html shows them under each requirement):

R3 (brakes receives BRAKE_CMD) leads to brakes in Braking within 50ms
  Each time brakes receives BRAKE_CMD, brakes in Braking holds then or at most 50ms later.
    A = brakes receives BRAKE_CMD
    B = brakes in Braking
    holds:
      A ··▲·······▲·····
      B ·····██·····█···
          └───┘ 50ms
    fails:
      A ··▲·······▲·····
      B ············█···
          └───┘ 50ms ✗ B not in time

eventually and leads to take a deadline, within 50ms. NuSMV, untimed, checks them without it; the monitors (archec gen --monitors), archec replay and --conflicts check it.

For a model checker, archec gen --target uppaal writes uppaal/model.xml and uppaal/model.q, and --target nusmv writes nusmv/model.smv (see Code generation).

Testing with faults#

A test case can break things on purpose, in Arche's simulation, to check that the model copes:

failure-mode FM-RX "Receiver hangs" { of Car.brakes; effect "No more braking"; inject "freeze brakes" }

case TC-CAN-LOSS "Brake CAN lost" {
  at 20ms fault drop adcu.can_brake        // every message through that link end is lost
  within 60ms expect brakes.state == "SafeStop"
  at 100ms fault up adcu.can_brake         // works again
  at 120ms fault FM-RX                     // a failure mode's `inject`
}

fault	what the simulation does
`drop part.port` / `up part.port`	messages through that link end are lost (traced as dropped, "fault: …") / no longer
`delay part.port 5ms`	each message through it arrives 5 ms later
`stuck part.port f=0, g=True`	messages through it carry those field values
`freeze part` / `thaw part`	the part (and what is inside it) stops: its code, timers and inbox; what it held resumes when thawed
`clear [target]`	ends the target's faults, or all of them
`FM-ID`	the failure mode's `inject`

A step takes fault … too (at its start). The linter checks the fault and its target (bad-fault, unresolved). Each one compiles to an observer call (fault_drop("adcu.can_brake")…) that Arche's engine runs.

Test coverage#

archec test main.arche --coverage (and Run with Coverage in VS Code's Test Explorer) says what the runs exercised of the model they ran on:

Coverage (car.yaml):
  states           6/8      75 %
      not covered: adcu: MinimalRisk
  transitions      5/10     50 %
      not covered: adcu: Autonomous -> MinimalRisk
  messages         4/10     40 %
      not covered: HEARTBEAT: adcu.can_brake -> brakes.can
  functions        9/9     100 %
  requirements     4/4     100 %

States entered, transitions taken, each message on each link that carries it, the functions called, and the requirements a test verifies whose cases ran. The whole report is kept in .archec/coverage.json. In the editor, each state, transition, function and link is marked run or not run at its line (VS Code 1.88+). Arche's simulator records it (arche-cli test --coverage <file>).

Runtime verification: the real system's logs#

archec replay checks the model's requirements on what the real system did: a CAN log (candump, Vector ASC or BLF), a ROS 2 bag (MCAP), or JSON lines, each event decoded by the model.

cd examples/brake-by-wire
archec replay main.arche logs/run-late.log logs/states-late.jsonl --junit replay.xml

  ✗ REQ-BRK-1   1 violation(s), the first at +0.070000 s (log time 1762790400.070000): brakes receives BRAKE_CMD at 50ms, not brakes in Braking 20ms later
  ✓ REQ-BRK-2   1 trigger(s)
  ✗ REQ-BRK-3   1 violation(s), the first at +0.150000 s (log time 1762790400.150000): brakes in Fault
  ✗ REQ-BRK-4   1 violation(s), the first at +0.050000 s (log time 1762790400.050000): BRAKE_CMD.force = 15000
  ✗ stale-after ctrl.status BRAKE_STATUS  1 violation(s), the first at +0.125000 s …: none for 70ms

A CAN id is the message the deployment's route … { id 0x100 } puts there, its bytes decoded by the same layout as the DBC and the generated C and Rust; a ROS 2 topic is the message of its type. What is checked: EARS requirements as monitors, formal properties, a metric that names a message field against its limit, contracts, chain budgets, ranges, periods and stale-after. A bus log does not show states: a JSON line {"t": …, "part": "brakes", "state": "Braking"} does (from a firmware trace, say), and what needs one is otherwise reported as not checkable. A response still awaited when the log ends is inconclusive. --json and --junit are for CI, as with archec ci. --scenario replay.arche --from ctrl turns the log into a test case: what ctrl sent, sent to the model at the same times, and the states the real parts went through, expected of the model's; archec test then runs the model on the real inputs. See docs/commands.md.