PLC runtime — verification¶
Test cases verifying the PLC runtime heart family (PLC runtime heart on iceoryx2 (FEAT_0010)). Coverage today: the bounded-time dispatch sub-feature (Bounded-time dispatch (FEAT_0017)) and its zero-allocation requirement (No heap allocation in dispatch (REQ_0060)); the scan-cycle observability sub-feature (Scan-cycle observability (FEAT_0021)); and the PREEMPT_RT validation harness sub-feature (PREEMPT_RT validation harness (FEAT_0022)).
The test cases are grouped by area (see the toctree), mirroring the requirement feats: bounded-time dispatch (zero-allocation plus the pre-allocated error slot), scan-cycle observability, the PREEMPT_RT validation harness, cyclic scan execution, event-driven I/O dispatch, deterministic logic sequencing, the cycle-time watchdog, real-time scheduling, cooperative shutdown, the cycle-overrun fault primitive, and the framework internal-fault model.
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 |
||
QoS 0 round-trip |
open |
||
QoS 1 round-trip |
open |
||
Retained-message publish + subscribe |
open |
||
Wildcard subscription with `+` |
open |
||
Wildcard subscription with `#` |
open |
||
Username/password authentication |
open |
||
TLS connection (developer-machine only) |
open |
||
Reconnect after broker bounce |
open |
||
HealthEvent emitted on every transition |
open |
||
Outbound bridge saturation → BackPressure |
open |
||
Inbound bridge saturation → DroppedInbound |
open |
||
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 |
||
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 |
||
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 %) |
open |
||
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 |