From cb2bc015f080b73e15c7d6d071924504e5b593ac Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Mon, 15 Jun 2026 03:51:27 +0200 Subject: [PATCH] feat(dbc): model CAN message flows as AADL ports + bus-bound connections (REQ-INGEST-DBC-FLOWS-001) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Extend DBC ingest to emit per-message dataflow on top of the v0.17.0 bus+devices+frame-types model. Each frame becomes an `out event data port` on its `BO_` transmitter node and an `in event data port` on every `SG_` receiver node, joined by `port` connections carrying `Deployment_Properties::Actual_Connection_Binding => (reference (can_bus))`. Event-data ports model the discrete data-carrying CAN frame; one broadcast `out` port fanning out to several `in` ports mirrors CAN's one-to-many. A frame is wired only when it has both a known transmitter and >=1 known receiver (the `Vector__XXX` placeholder and unknown names dropped), so no port is left dangling; frames lacking either end still emit their `data` type. Scope: this is faithful CAN dataflow modelling for traceability, diagrams and codegen — NOT a network-calculus feeder. spar's TFA/PLP are FIFO; CAN is priority-arbitrated, so a FIFO bound over it would be unsound. The CAN bus carries no `Spar_Network::Switch_Type`, so `extract_network_graph` correctly ignores it (cf. REQ-NC-BRIDGE-001). CAN response-time analysis stays a separate Tindell track behind its own soundness gate. Verified by the spar-dbc round-trip oracle: the emitted AADL (ports, connections, bus binding) must parse + instantiate with zero diagnostics. New test `sample_dbc_emits_message_flows`; TEST-INGEST-DBC-FLOWS in verification.yaml; REQ-INGEST-DBC-FLOWS-001 -> implemented. Co-Authored-By: Claude Opus 4.8 (1M context) --- artifacts/requirements.yaml | 29 +++-- artifacts/verification.yaml | 27 +++++ crates/spar-cli/src/main.rs | 4 +- crates/spar-dbc/src/lib.rs | 165 ++++++++++++++++++++++++++--- crates/spar-dbc/tests/roundtrip.rs | 54 ++++++++++ 5 files changed, 254 insertions(+), 25 deletions(-) diff --git a/artifacts/requirements.yaml b/artifacts/requirements.yaml index 0e828b2..3a83d89 100644 --- a/artifacts/requirements.yaml +++ b/artifacts/requirements.yaml @@ -2629,14 +2629,27 @@ artifacts: description: > Extend DBC ingest (REQ-INGEST-DBC-001) to model message transmit/receive as AADL features and connections: each frame - becomes a data port on its transmitting device (out) and on each - receiver (in), connected across the CAN bus. This is the - broadcast-bus analogue of the port-connection modelling the - network-calculus track consumes, and is deliberately deferred from - the v0.17.0 first cut (which ships bus + devices + frame data - types only). KILL-GATE: drop if the flat instance model already - carries enough for the target CAN analysis without per-flow ports. - status: proposed + becomes an `out event data port` on its transmitting node (the + `BO_` sender) and an `in event data port` on each receiving node + (the union of the frame's `SG_` signal receiver lists), joined by + `port` connections that carry + `Deployment_Properties::Actual_Connection_Binding => (reference + (can_bus))`. Event-data ports model the discrete data-carrying CAN + frame; the single broadcast `out` port fanning out to several `in` + ports mirrors CAN one-to-many. A frame is wired only when it has + both a known transmitter and >=1 known receiver (the `Vector__XXX` + placeholder and unknown names are dropped), so no port is left + dangling; frames lacking either end still emit their `data` type. + SCOPE: this is faithful CAN dataflow modelling for traceability, + diagrams and codegen — NOT a network-calculus feeder. spar's + TFA/PLP are FIFO; CAN is priority-arbitrated, so a FIFO bound over + it would be unsound. The CAN bus carries no `Spar_Network:: + Switch_Type`, so `extract_network_graph` correctly ignores it (cf. + REQ-NC-BRIDGE-001, which excludes CAN); CAN response-time analysis + is a separate Tindell track behind its own soundness gate. Verified + by the spar-dbc round-trip oracle (emitted AADL must parse + + instantiate with zero diagnostics). + status: implemented tags: [ingest, dbc, can, flows, tier1] fields: release: v0.20.0 diff --git a/artifacts/verification.yaml b/artifacts/verification.yaml index 355c4c3..94fef59 100644 --- a/artifacts/verification.yaml +++ b/artifacts/verification.yaml @@ -3442,3 +3442,30 @@ artifacts: links: - type: satisfies target: REQ-INGEST-DBC-001 + + - id: TEST-INGEST-DBC-FLOWS + type: feature + title: DBC message flows emit instantiable bus-bound port connections + description: > + spar-dbc's roundtrip test `sample_dbc_emits_message_flows` exercises + REQ-INGEST-DBC-FLOWS-001 on the representative .dbc: EngineData + (transmitted by EngineECU, received by Gateway + System) yields one + `out event data port` and matching `in` ports, and Status flows + Gateway -> EngineECU. It asserts the typed ports are emitted, every + flow connection carries + `Actual_Connection_Binding => (reference (can_bus))`, a `port` + connection runs from the transmitter instance, and the Vector__XXX + Broadcast frame (no node transmitter) produces its `data` type but + NO flow ports. The emitted AADL is then run back through spar's full + pipeline (parse, item-tree, scope, SystemInstance::instantiate) + asserting ZERO diagnostics — the parser/instantiator is the oracle, + so a malformed port, connection or binding fails the test. + fields: + method: automated-test + steps: + - run: cargo test -p spar-dbc --test roundtrip sample_dbc_emits_message_flows + status: passing + tags: [ingest, dbc, can, flows, tier1, v0200] + links: + - type: satisfies + target: REQ-INGEST-DBC-FLOWS-001 diff --git a/crates/spar-cli/src/main.rs b/crates/spar-cli/src/main.rs index 9da7a77..3e32ee4 100644 --- a/crates/spar-cli/src/main.rs +++ b/crates/spar-cli/src/main.rs @@ -82,7 +82,9 @@ fn print_usage() { eprintln!(" render Render architecture SVG from an instantiated system"); eprintln!(" verify Verify requirements against analysis results"); eprintln!(" codegen Generate code from an instantiated system model"); - eprintln!(" dbc Ingest a CAN .dbc file and emit AADL (bus + devices + frames)"); + eprintln!( + " dbc Ingest a CAN .dbc file and emit AADL (bus, devices, frames, message flows)" + ); eprintln!( " moves Hypothetical-rebinding oracle (verify a move under the migration overlay)" ); diff --git a/crates/spar-dbc/src/lib.rs b/crates/spar-dbc/src/lib.rs index eccf06a..bcd58fe 100644 --- a/crates/spar-dbc/src/lib.rs +++ b/crates/spar-dbc/src/lib.rs @@ -18,28 +18,50 @@ //! test fails. A useful side effect is a human-inspectable //! "transpile DBC → AADL" artifact. //! -//! # Mapping (v0.17.0 scope — `REQ-INGEST-DBC-001`) +//! # Mapping (`REQ-INGEST-DBC-001` + `REQ-INGEST-DBC-FLOWS-001`) //! -//! | DBC concept | AADL construct | -//! |------------------------|-------------------------------------------------| -//! | CAN bus (the network) | a single `bus CAN_Bus` | -//! | node / ECU | `device ` with `requires bus access` | -//! | message (frame) | `data Msg_` with `Data_Size => Bytes` | -//! | the whole network | `system CAN_Network` + its implementation | +//! | DBC concept | AADL construct | +//! |----------------------------|-------------------------------------------------| +//! | CAN bus (the network) | a single `bus CAN_Bus` | +//! | node / ECU | `device ` with `requires bus access` | +//! | message (frame) | `data Msg_` with `Data_Size => Bytes` | +//! | message tx (the `BO_` node)| an `out event data ` port on that device | +//! | message rx (a `SG_` receiver) | an `in event data ` port on that device | +//! | a tx→rx pairing | a `port` connection bound to the CAN bus | +//! | the whole network | `system CAN_Network` + its implementation | //! -//! Message *flows* (which node transmits/receives which frame, modelled as -//! ports and data connections across the bus) are deliberately **out of -//! scope** for this first cut — that is the broadcast-bus equivalent of the -//! port-connection modelling the network-calculus track will need, and is -//! tracked separately as a follow-up requirement. What ships here is a -//! structurally complete, instantiable model: bus + devices + message data -//! types, with each device wired to the bus. +//! # Message flows (`REQ-INGEST-DBC-FLOWS-001`) +//! +//! A CAN frame is a discrete, data-carrying event, so each modelled message +//! becomes an `out event data Msg_` port on its transmitting node and an +//! `in event data Msg_` port on every receiving node, joined by `port` +//! connections. Each connection carries +//! `Deployment_Properties::Actual_Connection_Binding => (reference (can_bus))` +//! — the faithful AADL statement that this message is carried over the CAN +//! bus. The single broadcast `out` port fanning out to several `in` ports +//! mirrors CAN's one-to-many broadcast. +//! +//! Transmitter comes from the `BO_` line; receivers are the union of the +//! frame's `SG_` signal receiver lists. A message is wired as a flow only when +//! it has **both** a known transmitter node and at least one known receiver +//! node (the `Vector__XXX` placeholder and unknown names are dropped), so every +//! emitted port participates in a connection — no dangling features. Messages +//! lacking either end still emit their `data` type, as before. +//! +//! **Scope note (not a network-calculus feeder).** These connections model the +//! CAN broadcast for dataflow, traceability and codegen. They are *not* wired +//! into spar's FIFO TFA/PLP network-calculus engine: CAN is priority-arbitrated, +//! not FIFO, so a FIFO bound over it would be unsound. The CAN bus carries no +//! `Spar_Network::Switch_Type`, so `spar_network::extract_network_graph` +//! correctly ignores it (buses without that property are skipped). CAN +//! response-time analysis is a separate (Tindell) track behind its own +//! soundness gate. //! //! [Vector CAN database]: https://en.wikipedia.org/wiki/CAN_bus #![forbid(unsafe_code)] -use std::collections::HashSet; +use std::collections::{HashMap, HashSet}; use std::fmt; use can_dbc::{Dbc, Transmitter}; @@ -81,6 +103,17 @@ const BUS_NAME: &str = "CAN_Bus"; /// The fixed root system classifier name. const SYSTEM_NAME: &str = "CAN_Network"; +/// A modelled message flow: the message's index, its transmitting device, and +/// the port names on each end of the resulting `port` connections. +struct MessageFlow { + /// Index into `messages` (and `dbc.messages`). + msg: usize, + /// Transmitting device index + its `out event data` port name. + tx: (usize, String), + /// Receiving device indices + their `in event data` port names. + rx: Vec<(usize, String)>, +} + fn emit_aadl(dbc: &Dbc, package_name: &str) -> String { // One global namespace for *classifier* names (bus, data types, devices, // system) so a node accidentally named like a message can never collide. @@ -111,6 +144,76 @@ fn emit_aadl(dbc: &Dbc, package_name: &str) -> String { .map(|n| classifiers.alloc(&n.0, "Ecu")) .collect(); + // Raw DBC node name -> device index, for resolving transmitters/receivers. + let node_index: HashMap<&str, usize> = dbc + .nodes + .iter() + .enumerate() + .map(|(i, n)| (n.0.as_str(), i)) + .collect(); + + // -- flow model (REQ-INGEST-DBC-FLOWS-001) --------------------------- + // For each message with a known transmitter AND >=1 known receiver, allocate + // a typed `out`/`in event data` port on each participating device and record + // the flow for connection emission. Port names live in a per-device + // namespace seeded with the reserved `can` bus-access feature. + let mut dev_port_alloc: Vec = (0..devices.len()) + .map(|_| { + let mut a = NameAllocator::new(); + a.reserve("can"); + a + }) + .collect(); + // Extra feature lines (typed ports) per device, in message order. + let mut dev_features: Vec> = vec![Vec::new(); devices.len()]; + let mut flows: Vec = Vec::new(); + + for (j, m) in dbc.messages.iter().enumerate() { + let tx_dev = match &m.transmitter { + Transmitter::NodeName(n) => node_index.get(n.as_str()).copied(), + Transmitter::VectorXXX => None, + }; + // Receivers: union over the frame's signals, in first-seen order, + // dropping the placeholder, the transmitter itself, and unknown nodes. + let mut rx_devs: Vec = Vec::new(); + for sig in &m.signals { + for r in &sig.receivers { + if !is_real_node(r) { + continue; + } + if let Some(&ri) = node_index.get(r.as_str()) + && Some(ri) != tx_dev + && !rx_devs.contains(&ri) + { + rx_devs.push(ri); + } + } + } + + let Some(txi) = tx_dev else { continue }; + if rx_devs.is_empty() { + continue; + } + + let msg_type = messages[j].0.clone(); + let base = sanitize_ident(&m.name, "Frame"); + let tx_port = dev_port_alloc[txi].alloc(&format!("{base}_tx"), "frame_tx"); + dev_features[txi].push(format!("{tx_port}: out event data port {msg_type};")); + let rx: Vec<(usize, String)> = rx_devs + .iter() + .map(|&ri| { + let p = dev_port_alloc[ri].alloc(&format!("{base}_rx"), "frame_rx"); + dev_features[ri].push(format!("{p}: in event data port {msg_type};")); + (ri, p) + }) + .collect(); + flows.push(MessageFlow { + msg: j, + tx: (txi, tx_port), + rx, + }); + } + let mut out = String::new(); push_line(&mut out, 0, &format!("package {pkg}")); push_line(&mut out, 0, "public"); @@ -135,7 +238,7 @@ fn emit_aadl(dbc: &Dbc, package_name: &str) -> String { } // -- nodes as devices ------------------------------------------------ - for dev in &devices { + for (i, dev) in devices.iter().enumerate() { push_line(&mut out, 1, &format!("device {dev}")); push_line(&mut out, 2, "features"); push_line( @@ -143,6 +246,10 @@ fn emit_aadl(dbc: &Dbc, package_name: &str) -> String { 3, &format!("can: requires bus access {BUS_NAME};"), ); + // Message-flow ports (transmitted out, received in). + for feature in &dev_features[i] { + push_line(&mut out, 3, feature); + } push_line(&mut out, 1, &format!("end {dev};")); out.push('\n'); } @@ -176,6 +283,7 @@ fn emit_aadl(dbc: &Dbc, package_name: &str) -> String { if !dev_insts.is_empty() { push_line(&mut out, 2, "connections"); let mut conns = NameAllocator::new(); + // Bus-access connections (every device shares the broadcast bus). for inst in &dev_insts { let c = conns.alloc(&format!("{inst}_access"), "access"); push_line( @@ -184,6 +292,25 @@ fn emit_aadl(dbc: &Dbc, package_name: &str) -> String { &format!("{c}: bus access {inst}.can <-> {bus_inst};"), ); } + // Message-flow port connections, each bound to the CAN bus. A single + // `out` port may source several connections (CAN broadcast fan-out). + for flow in &flows { + let (txi, tx_port) = &flow.tx; + let tx_inst = &dev_insts[*txi]; + let base = sanitize_ident(&dbc.messages[flow.msg].name, "frame").to_lowercase(); + for (ri, rx_port) in &flow.rx { + let rx_inst = &dev_insts[*ri]; + let c = conns.alloc(&format!("{tx_inst}_{base}_to_{rx_inst}"), "flow"); + push_line( + &mut out, + 3, + &format!( + "{c}: port {tx_inst}.{tx_port} -> {rx_inst}.{rx_port} \ + {{Deployment_Properties::Actual_Connection_Binding => (reference ({bus_inst}));}};" + ), + ); + } + } } push_line(&mut out, 1, &format!("end {SYSTEM_NAME}.impl;")); @@ -193,6 +320,12 @@ fn emit_aadl(dbc: &Dbc, package_name: &str) -> String { out } +/// Whether `name` denotes a real DBC node, excluding the `Vector__XXX` +/// "no node" placeholder (and its variants) and the empty string. +fn is_real_node(name: &str) -> bool { + !matches!(name, "Vector__XXX" | "VectorXXX" | "") +} + fn push_line(out: &mut String, indent: usize, text: &str) { for _ in 0..indent { out.push_str(" "); diff --git a/crates/spar-dbc/tests/roundtrip.rs b/crates/spar-dbc/tests/roundtrip.rs index fa48d9e..6d92d2a 100644 --- a/crates/spar-dbc/tests/roundtrip.rs +++ b/crates/spar-dbc/tests/roundtrip.rs @@ -125,6 +125,60 @@ fn sample_dbc_emits_instantiable_aadl() { assert_eq!(device_count, 3, "expected one device per DBC node"); } +#[test] +fn sample_dbc_emits_message_flows() { + // REQ-INGEST-DBC-FLOWS-001: messages become typed event-data ports joined by + // bus-bound `port` connections. The instantiation assertions in `instantiate` + // are the oracle — if any port/connection/binding is malformed, it fails. + let aadl = dbc_to_aadl(SAMPLE_DBC, "CanDemo").expect("DBC should parse"); + + // EngineData is transmitted by EngineECU and received by Gateway + System: + // one `out` port, matching `in` ports on the receivers. + assert!( + aadl.contains("out event data port Msg_EngineData;"), + "missing transmitter port for EngineData:\n{aadl}" + ); + assert!( + aadl.contains("in event data port Msg_EngineData;"), + "missing receiver port for EngineData:\n{aadl}" + ); + // Status flows Gateway -> EngineECU. + assert!( + aadl.contains("out event data port Msg_Status;") + && aadl.contains("in event data port Msg_Status;"), + "missing Status flow ports:\n{aadl}" + ); + // Every flow connection is bound to the CAN bus. + assert!( + aadl.contains("Actual_Connection_Binding => (reference (can_bus));"), + "flow connection not bound to the CAN bus:\n{aadl}" + ); + // A `port` connection from the transmitter instance must exist. + assert!( + aadl.contains("port engineecu.") && aadl.contains("-> gateway."), + "missing EngineData broadcast connection:\n{aadl}" + ); + // Broadcast has a Vector__XXX transmitter (no node) -> data type only, no + // ports/connections. Its `data` type still ships. + assert!( + aadl.contains("data Msg_Broadcast"), + "Broadcast data type should still be emitted:\n{aadl}" + ); + assert!( + !aadl.contains("event data Msg_Broadcast"), + "Broadcast has no transmitter and must not produce flow ports:\n{aadl}" + ); + + // The whole thing must still instantiate with zero diagnostics. + let instance = instantiate(&aadl, "CanDemo"); + let device_count = instance + .components + .iter() + .filter(|(_, c)| format!("{:?}", c.category).contains("Device")) + .count(); + assert_eq!(device_count, 3, "expected one device per DBC node"); +} + #[test] fn empty_network_still_instantiates() { // A header-only DBC (no nodes, no messages) must still yield a valid,