feat(dbc): CAN message flows as AADL ports + bus-bound connections (REQ-INGEST-DBC-FLOWS-001)

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

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

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)"
     );

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 <Node>` with `requires bus access`      |
-//! | message (frame)        | `data Msg_<Name>` with `Data_Size => <n> 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 <Node>` with `requires bus access`      |
+//! | message (frame)            | `data Msg_<Name>` with `Data_Size => <n> Bytes` |
+//! | message tx (the `BO_` node)| an `out event data <Msg>` port on that device   |
+//! | message rx (a `SG_` receiver) | an `in event data <Msg>` 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_<Name>` port on its transmitting node and an
+//! `in event data Msg_<Name>` 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<NameAllocator> = (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<String>> = vec![Vec::new(); devices.len()];
+    let mut flows: Vec<MessageFlow> = 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<usize> = 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,14 +238,18 @@ 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(
             &mut out,
             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("  ");

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,