Verification¶
Test cases verifying requirements. Each test directive
:verifies: one or more req parents (or building-block /
architecture parents on arc42-structured pages).
- Connector framework — verification
- PLC runtime — verification
- Bounded global allocator — verification
- Device-driver codegen — verification
- CANopen device-driver codegen — verification
- Logging — verification
- EtherCAT network-config codegen — verification
- Runtime diagnostics (medkit) tests
- Message-plane interface-description codegen — verification
ID |
Title |
Status |
Verifies |
|---|---|---|---|
ExponentialBackoff invariants |
open |
||
ConnectorHealth state-machine transitions |
open |
||
MqttRouting wildcard demux predicate |
open |
||
ChannelDescriptor validation |
open |
||
Interval trigger fires the configured number of times |
implemented |
||
Interval cardinality matches run_n on the threaded pool |
implemented |
||
ExecutionMonitor brackets every dispatch |
implemented |
||
Subscriber-triggered ingestion wakes the item |
implemented |
||
Publisher API send paths deliver to attached subscribers |
implemented |
||
Publisher::loan round-trips without serialisation |
implemented |
||
JsonCodec round-trip property test |
open |
||
Codec encode error on undersized buffer |
open |
||
Codec decode error propagation |
open |
||
NotifyOutcome surfaces listeners-notified count |
implemented |
||
Chain runs its items in declared order |
implemented |
||
Diamond DAG runs every vertex exactly once |
implemented |
||
StopChain and Err propagate to downstream items |
implemented |
||
wrap_with_condition gates execution on the predicate |
implemented |
||
TriggerDeclarer::deadline stores the (listener, deadline) pair |
implemented |
||
ExecutionMonitor::post_execute reports per-execute duration |
implemented |
||
ChannelWriter → ChannelReader round-trip |
open |
||
Sequence-number monotonicity |
open |
||
Timestamp populated at send |
open |
||
Correlation ID round-trip |
open |
||
Per-channel size — 4 KB, 64 KB, 1 MB |
open |
||
Payload-overflow rejection |
open |
||
Service naming derived from descriptor |
open |
||
ThreadAttributes affinity_mask compiles and runs |
implemented |
||
ThreadAttributes priority setter compiles into the worker thread body |
implemented |
||
Stoppable::stop wakes an idle WaitSet from another thread |
implemented |
||
Per-iteration error slot is pre-allocated, not Arc-Mutex-allocated per cycle |
implemented |
||
In-process gateway smoke |
open |
||
Separate-process gateway smoke |
open |
||
SIGINT clean exit within 5-second budget |
open |
||
No control-plane envelopes flow |
open |
||
Bridge handoff under arbitrary interleaving |
open |
||
Health state-machine under concurrent updates |
open |
||
Zero allocations in steady-state dispatch |
open |
||
Cap exhaustion and oversize alloc both fail-closed |
open |
||
Steady-state cap behaviour under burst |
open |
||
lock() then alloc panics |
open |
||
Counter accuracy |
open |
||
Concurrent alloc/dealloc safety smoke |
open |
||
Histogram percentile accuracy |
implemented |
||
Per-task max jitter under synthetic period violation |
implemented |
||
Overrun counter increments exactly per overrun cycle |
implemented |
||
Push and pull stat paths agree |
implemented |
||
Allocation-free telemetry update |
implemented |
||
BinaryCodec round-trip and constant-length contract |
implemented |
||
EthercatConnector trait surface |
open |
||
EthercatRouting field round-trip |
open |
||
Single MainDevice per gateway instance |
open |
||
Bus reaches OP before traffic accepted |
open |
||
Static PDO map accepted from options |
open |
||
PDO mapping applied during PRE-OP to SAFE-OP |
open |
||
Cycle time configurable |
open |
||
Missed ticks are skipped not queued |
open |
||
Distributed Clocks bring-up is opt-in |
open |
||
Up requires OP and matching working counter |
open |
||
Working-counter mismatch transitions to Degraded |
open |
||
Tokio sidecar contained inside connector crate |
open |
||
Bridge channels are bounded with configurable capacity |
open |
||
Outbound bridge saturation surfaces as BackPressure |
open |
||
Inbound bridge saturation surfaces as DroppedInbound |
open |
||
Gateway opens raw socket on Linux with CAP_NET_RAW |
open |
||
PDI bit-slice byte-aligned round-trip |
open |
||
PDI bit-slice unaligned round-trip |
open |
||
Adjacent PDI bit slices do not interfere |
open |
||
Per-channel routing registry has stable iteration order |
open |
||
Outbound end-to-end (plugin send → PDI slice via mock) |
open |
||
Inbound end-to-end (PDI slice via mock → plugin recv) |
open |
||
Loopback round-trip (plugin → mock → plugin) |
open |
||
Asymmetric expected_wkc summing |
open |
||
DC cycle path branches on options.distributed_clocks |
open |
||
Recovery state machine drives BusDriver::recover per policy |
open |
||
Health transitions during recovery |
open |
||
Hardware drill — endurance + unplug/replug |
open |
||
Harness builds and runs on Linux non-RT |
open |
||
NDJSON schema validation |
open |
||
Harness telemetry agrees with stats_snapshot |
open |
||
Username/password CONNECT against a real broker |
implemented |
||
TLS handshake and round-trip |
implemented |
||
MQTT 3.1.1 plain JSON round-trip |
implemented |
||
ZenohRouting field validation |
open |
||
ZenohConnector implements Connector with ZenohRouting |
open |
||
Pub/sub end-to-end against MockZenohSession |
open |
||
Query round-trip against MockZenohSession |
open |
REQ_0420; REQ_0421; REQ_0422; REQ_0423; REQ_0424; REQ_0426; REQ_0427 |
|
Codec failure paths for queries |
open |
||
Outbound bridge saturation surfaces as BackPressure |
open |
||
Inbound bridge saturation surfaces as DroppedInbound |
open |
||
Query timeout emits 0x03 terminator |
open |
||
Health state machine on MockZenohSession lifecycle |
implemented |
||
REQ_0441 anti-req — no ReconnectPolicy on session loss |
implemented |
||
zenoh-integration feature gates the real zenoh dep |
implemented |
||
Cross-platform support |
implemented |
||
Two-peer real session pub/sub |
draft |
||
Client-mode router smoke |
draft |
||
Tokio sidecar contained inside taktora-connector-zenoh |
implemented |
||
parse() accepts a representative Beckhoff EL3001 ESI |
open |
||
Parser compiles under no_std + alloc |
rejected |
||
Parser is independent of ethercrab |
open |
||
Vendor-specific elements survive as RawXml |
open |
||
Parse errors carry line and column |
open |
||
Name sanitisation handles ESI naming edge cases |
open |
||
Revision collision produces distinct idents |
open |
||
PDO entry dedup collapses structurally identical layouts |
open |
||
TokenStream emission, not string formatting |
open |
||
EL3001 backend output snapshot |
open |
||
Generated registry covers every emitted device |
open |
||
Generated module compiles under no_std + alloc |
open |
||
Backend is the sole ethercrab consumer in the toolchain |
open |
||
Object-dictionary emission gated by feature flag |
open |
||
EsiDevice trait shape compiles for a hand-written device |
open |
||
EsiConfigurable async trait shape compiles |
open |
||
ethercat-esi-rt is the trait home, not taktora-internal |
open |
||
Builder writes a parseable Rust file to OUT_DIR |
open |
||
cargo rerun-if-changed emitted per ESI input |
open |
||
Output passes prettyplease formatting |
open |
||
cargo esi expand emits a single device's code |
open |
||
cargo esi list enumerates devices |
open |
||
CLI output matches build helper output byte-for-byte |
open |
||
Verifier passes on matching ESI + SII pair |
open |
||
Verifier reports the differing field |
open |
||
Verifier reuses ethercat-esi parser |
open |
||
Verifier exit codes follow the documented matrix |
open |
||
Repeated codegen runs produce byte-identical output |
open |
||
Input-file ordering does not affect output |
open |
||
Layering integrity check (Cargo.toml audit) |
open |
||
CanConnector trait surface |
open |
||
CanRouting field round-trip |
open |
||
Classical CAN round-trip via MockCanInterface |
open |
||
CAN-FD round-trip via MockCanInterface |
open |
||
Per-iface filter union |
open |
||
Multi-iface inbound demux |
open |
||
Bus-off → Down → ReconnectPolicy reopen |
open |
||
error-passive → Degraded → recovery |
open |
||
Tokio sidecar contained inside taktora-connector-can |
open |
||
Outbound bridge saturation surfaces as BackPressure |
open |
||
Inbound bridge saturation surfaces as DroppedInbound |
open |
||
socketcan-integration feature gates the real socketcan dep |
implemented |
||
Linux raw-socket smoke against vcan0 |
implemented |
||
Error frames not exposed to plugin |
open |
||
Per-iface routing registry has stable iteration order |
open |
||
Identity, DictEntry, PdoEntry round-trip |
open |
||
fieldbus-od-core has no transport deps |
open |
||
fieldbus-od-core compiles under no_std + alloc |
open |
||
ethercat-esi re-exports lifted types |
open |
||
parse() accepts a representative Maxon EPOS4 EDS |
open |
||
Parser compiles under no_std + alloc |
open |
||
Parser is independent of codegen and transport |
open |
||
Unknown sections survive as RawSection |
open |
||
Parse errors carry line and column |
open |
||
Liberal-quirk parsing emits warnings without failing |
open |
||
Name sanitisation handles EDS naming edge cases |
open |
||
Revision collision produces distinct idents |
open |
||
PDO entry dedup collapses structurally identical layouts |
open |
||
TokenStream emission, not string formatting |
open |
||
One EDS file equals one device |
open |
||
EPOS4 backend output snapshot |
open |
||
Generated registry covers every emitted device |
open |
||
Generated module compiles under no_std + alloc |
open |
||
Backend is the sole canopen-eds-rt consumer in the toolchain |
open |
||
Object-dictionary emission gated by feature flag |
open |
||
Dummy entries skipped in PDO struct fields |
open |
||
Bring-up SDO writes emitted from EDS |
open |
||
CanOpenDevice trait shape compiles for a hand-written device |
open |
||
CanOpenConfigurable async trait shape compiles |
open |
||
canopen-eds-rt is the trait home, not taktora-internal |
open |
||
PdoOut payload uses heapless::Vec<u8, 8> |
open |
||
RPDO rejected outside Operational state |
open |
||
Builder writes a parseable Rust file to OUT_DIR |
open |
||
cargo rerun-if-changed emitted per EDS input |
open |
||
Output passes prettyplease formatting |
open |
||
Parser warnings surface as cargo:warning lines |
open |
||
cargo eds expand emits a single device's code |
open |
||
cargo eds list enumerates devices |
open |
||
CLI output matches build helper output byte-for-byte |
open |
||
Verifier passes on matching EDS + dump pair |
open |
||
Verifier reports the differing field |
open |
||
Verifier reuses canopen-eds parser |
open |
||
Verifier exit codes follow the documented matrix |
open |
||
Verifier rejects unknown schema version |
open |
||
Repeated codegen runs produce byte-identical output |
open |
||
Input-file ordering does not affect output |
open |
||
Layering integrity check (Cargo.toml audit) |
open |
||
Facade-only emission lands DLT bytes at the daemon |
implemented |
||
taktora-log re-exports compile as drop-in log macros |
implemented |
||
LogSink is object-safe |
implemented |
||
Second taktora_log::init() returns AlreadyInitialized |
implemented |
||
Pre-installed log::Log wins over taktora_log::init() |
implemented |
||
tracing::* events reach the active LogSink |
implemented |
||
Encoder produces parseable AUTOSAR DLT R20-11 bytes |
implemented |
||
UDS and TCP transports both connect and write |
implemented |
||
AppId and CtxId enforce 4-character ASCII |
implemented |
||
log::kv pairs map to native DLT verbose arguments |
implemented |
||
Set-Log-Level and Set-Default control messages apply |
implemented |
||
Default level is INFO until overridden |
implemented |
||
Producer-side send never blocks the calling thread |
implemented |
||
Offline ring buffers and drains FIFO across reconnect |
implemented |
||
Budget breach faults task and halts dispatch |
implemented |
||
Clear task fault resumes dispatch |
implemented |
||
Iteration budget faults executor with silent cascade |
implemented |
||
Fault handler dispatches in place of main item |
implemented |
||
Overrun count persists across clears |
implemented |
||
Fault state set from worker visible from main |
implemented |
||
Overrun post-execute path zero allocations |
implemented |
||
Fault callbacks forwarded to tracing |
implemented |
||
Framework panic routes to fatal handler |
open |
||
Default fail-fast aborts the process |
open |
||
Item panic is contained, not aborted |
open |
||
parse() accepts a representative WAGO network.yaml |
open |
||
Multi-bus document is rejected |
open |
||
Channels resolve to devices by label, stable under reorder |
open |
||
Parser is independent of the connector runtime |
open |
||
Generated module emits the expected static PDO_MAP |
open |
||
Generated routing and channel-name constants match the bindings |
open |
||
Configured addresses follow bus position, override honoured |
open |
||
expected_wkc is derived from PDO directions |
open |
||
Generated output is byte-deterministic |
open |
||
Build helper generates into OUT_DIR and the module compiles |
open |
||
Build helper emits rerun-if-changed for config and ESI |
open |
||
expand subcommand prints the build-equivalent module |
open |
||
fetch vendors a remote ESI and records a pinned lockfile |
open |
||
Build fetches nothing; unvendored URL is a build error |
open |
||
Overlapping slices are a build error unless allowed |
open |
||
Out-of-image, zero-length, dangling, and collision faults fail the build |
open |
||
Unmapped process-image gaps warn but do not fail |
open |
||
Generated bring-up assertions catch identity, alias, and WKC mismatch |
open |
||
No runtime parsing; generated config is static with no heap |
open |
||
Exact windowed min/max retain observed extremes |
implemented |
||
Deadline lateness — drift accumulates, coalesced pair heals, offsets stay honest |
implemented |
||
Cycle index is monotonic across faulted scans |
implemented |
||
GridTimer holds the absolute grid (advance, skip-realign, multi-period) |
implemented |
||
Dispatcher skip-realign is carried, consumed once, and re-anchors lateness |
implemented |
||
Run loop survives EINTR storms |
implemented |
||
Dispatch thread runs with 1 µs timer slack |
implemented |
||
Grid lateness anchors at the first dispatch's nominal slot |
implemented |
||
OP wait-loop pacing decisions |
open |
||
Bring-up failure surfaces as terminal Down |
open |
||
Per-SM watchdog-trigger enable decodes from control-byte bit 6 |
open |
||
SM-watchdog registers resolve and are emitted for output devices |
open |
||
SM-watchdog bound and enable are validated at config time |
open |
||
SM-watchdog tick maths against the AOU_0016 bound |
open |
||
SM-watchdog safe-state drill on real WAGO hardware |
open |
||
Health subscriptions broadcast to every subscriber |
open |
||
FMMU declarations parse in order with tolerated unknowns |
open |
||
EEPROM source data decodes; bad hex is a located error |
open |
||
MDP catalog and slots parse from synthetic and real modular ESI |
open |
||
Sub-octave percentile accuracy (≤ 1 %) |
implemented |
||
Startup SDOs written in order before PDO assignment |
open |
||
EL7047 OpMode enum, exact lengths, pdo_assignment, round-trip |
implemented |
||
AlternativeSmMapping parsing |
implemented |
||
At-most-one borrowed-job submit per barrier phase; multiple intervals rejected |
implemented |
||
ViewModel derive: layout, schema and envelope sizing |
implemented |
||
Command derive: CommandParams, idempotent flag and schema |
implemented |
||
Non-POD ViewModel fields rejected at compile time |
implemented |
||
Server-side Property seqlock RT-update handle |
implemented |
||
Publish-plane iceoryx2 round-trip: cadence, coalescing, zero-subscriber skip |
implemented |
||
Command-plane iceoryx2 round-trip: acceptance ack, dedupe, off-RT handler |
implemented |
||
Command deterministic behaviour: reason codes, back-pressure, gating |
implemented |
||
Assembled UiConnector end-to-end over iceoryx2 |
implemented |
||
Reference client end-to-end: discovery, hash validation, diffing, restart, trust |
implemented |
REQ_0864; REQ_0876; REQ_0877; REQ_0880; REQ_0881; REQ_0882; REQ_0884 |
|
Connector health reflects local publish health |
implemented |
||
Golden manifest and contract hash |
implemented |
||
Slice channel variable-length round-trip |
implemented |
||
Slice channel grows then enforces the ceiling |
implemented |
||
J1939 29-bit ID decode and PGN routing |
implemented |
||
J1939Routing transport-class N validation |
implemented |
||
BAM round-trip via MockJ1939Interface |
implemented |
||
RTS/CTS connection-mode round-trip |
implemented |
||
ETP round-trip over the slice channel, bounded |
implemented |
||
TP timeout surfaces as a health event |
implemented |
||
Concurrent inbound TP sessions are bounded |
implemented |
||
Address-claim contention and cannot-claim |
implemented |
||
Claim state drives health and gates TX |
implemented |
||
MockJ1939Interface deterministic harness |
implemented |
||
Model wire shapes round-trip |
open |
||
Core crates carry no taktora dependency |
open |
||
Gateway read core over the mock provider |
open |
||
Worst-wins health rollup |
open |
||
Off-path forwarding never blocks the control path |
open |
||
Drop-in contract snapshot |
open |
||
Read-core over a live server matches the contract shapes |
implemented |
||
Deferred families return a contract-shaped 501 |
implemented |
||
Transport hardening is present and configurable |
implemented |
||
Builder and TOML manifests agree |
implemented |
||
Manifest re-parents raw entities over a live server |
implemented |
||
Empty manifest yields flat grouping |
implemented |
||
Executor binding satisfies the provider seam |
implemented |
||
A running executor drives binding liveness and timing |
implemented |
||
Hook write path performs zero heap allocation |
rejected |
||
Connector health surfaces a Component and DTCs |
implemented |
||
DTC lifecycle and occurrence bookkeeping |
implemented |
||
Confirmed DTC carries a last-sample freeze-frame |
implemented |
||
Freeze-frame end-to-end through the fault-detail endpoint |
implemented |
||
Trigger subscription CRUD round-trip |
implemented |
||
Refresh-diff loop streams fault events as SSE |
implemented |
||
Health transition streams health_changed |
implemented |
||
Token endpoint issues a contract-shaped JWT |
implemented |
||
Enforcement = none accepts requests with or without a token |
implemented |
||
Full client login-to-read flow and the Authenticator seam |
implemented |
||
Lock acquire-extend-release round-trip |
implemented |
||
Lock conflict and break_lock override |
implemented |
||
Lock ownership and X-Client-Id enforcement |
implemented |
||
Boundedness and structural-soundness contract |
implemented |
||
DBC parse and lower round-trip |
implemented |
||
Naming policy and identifier-collision detection |
implemented |
||
CAN backend emits parseable WireType tokens |
implemented |
||
Generated round-trip, DLC sizing, little-endian placement |
implemented |
||
Enum and signed-enum round-trip; unknown value rejected |
implemented |
||
Wire error path — buffer and value bounds rejected |
implemented |
||
Multiplexed signals flatten into one struct |
implemented |
||
Root advertises the served surface honestly |
implemented |
||
Health carries the golden telemetry blocks |
implemented |
||
Global fault clear-all acknowledges |
implemented |
||
Auth disable is 404, not 501 |
implemented |
||
Lock reads expose the owner view |
implemented |
||
Entity-scoped triggers are pinned and isolated |
implemented |
||
Global stream replays the ring and honours Last-Event-ID |
implemented |
||
Operations catalogue lists and details |
implemented |
||
Operation execution lifecycle over HTTP |
implemented |
||
Unknown operation is 404 |
implemented |
||
Configurations lifecycle over HTTP |
implemented |
||
Bulk-data lifecycle over HTTP |
implemented |
||
Scripts lifecycle over HTTP |
implemented |
||
Software-update lifecycle over HTTP |
implemented |
||
Lifecycle-status transitions over HTTP |
implemented |
||
Logs read and configuration over HTTP |
implemented |
||
Cyclic-subscriptions CRUD and sampling SSE |
implemented |
||
Health telemetry overlay |
implemented |
||
Single-entity capability catalogue |
implemented |
||
MsgPackCodec round-trip and error contract |
implemented |
||
Build identity in the version catalogue |
implemented |
||
MqttConnector implements Connector |
implemented |
||
MqttRouting carries topic, qos, retained |
implemented |
||
Topic and filter grammar validation |
implemented |
||
Wildcard topic-matcher semantics |
implemented |
||
Outbound publish preserves QoS and retained |
implemented |
||
Tokio sidecar contained in the gateway crate |
implemented |
||
Bridge channels are bounded and capacity-clamped |
implemented |
||
Outbound-bridge saturation surfaces as BackPressure |
implemented |
||
Inbound-bridge saturation drops frames and signals Degraded |
implemented |
||
Inbound PUBLISH matched locally and fanned out |
implemented |
||
Broker subscriptions deduplicated and reference-counted |
implemented |
||
Connection state maps to ConnectorHealth |
implemented |
||
Reconnect and backoff parameters are configurable |
implemented |
||
Auth-rejected CONNACK transitions to Down |
implemented |
||
Reconnect-attempt ceiling transitions to Down |
implemented |
||
Clean session on CONNECT is set and configurable |
implemented |
||
SUBSCRIBE replay on reconnect |
implemented |
||
JsonCodec is the default codec |
implemented |