analysis.yaml

# STPA Analysis — Spar AADL Toolchain
#
# Analyzes spar itself as a safety-relevant tool. Spar's analysis results
# inform architecture decisions for DO-178C/DO-254 avionics systems.
# An incorrect analysis result (false negative) could lead to an unsafe
# architecture being approved. A false positive wastes engineering effort
# but is not safety-critical.

artifacts:

  # ══════════════════════════════════════════════════════════════════════
  # STEP 1a: Losses
  # ══════════════════════════════════════════════════════════════════════

  - id: L-1
    type: loss
    title: Unsafe architecture approved
    description: >
      An architecture with safety-critical defects (scheduling overrun,
      single-point-of-failure, unconnected safety paths) is approved for
      implementation because spar failed to detect the defect.
    stakeholders: [system-integrator, certification-authority, end-user]

  - id: L-2
    type: loss
    title: Excessive engineering rework
    description: >
      False positive diagnostics cause engineers to redesign correct
      architectures, wasting significant time and budget.
    stakeholders: [system-integrator, project-manager]

  - id: L-3
    type: loss
    title: Loss of trust in toolchain
    description: >
      Inconsistent, incorrect, or confusing analysis results cause
      engineers to bypass spar and rely on manual review, eliminating
      the safety benefit of automated analysis.
    stakeholders: [system-integrator, safety-reviewer]

  - id: L-4
    type: loss
    title: Incorrect architecture documentation
    description: >
      Serialized JSON or rendered SVG output misrepresents the actual
      AADL model, leading to incorrect documentation artifacts in the
      certification evidence package.
    stakeholders: [certification-authority, safety-reviewer]

  # ══════════════════════════════════════════════════════════════════════
  # STEP 1b: Hazards
  # ══════════════════════════════════════════════════════════════════════

  - id: H-1
    type: hazard
    links:
      - type: leads-to-loss
        target: L-1
    title: Analysis produces false negative
    description: >
      Spar's analysis passes fail to detect a genuine architectural
      defect in the AADL model (e.g., schedulability violation,
      unconnected safety-critical port, single-point-of-failure path).
    severity: critical
    losses: [L-1]

  - id: H-2
    type: hazard
    links:
      - type: leads-to-loss
        target: L-2
      - type: leads-to-loss
        target: L-3
    title: Analysis produces false positive
    description: >
      Spar reports a defect that does not actually exist in the model,
      causing unnecessary rework.
    severity: marginal
    losses: [L-2, L-3]

  - id: H-3
    type: hazard
    links:
      - type: leads-to-loss
        target: L-1
      - type: leads-to-loss
        target: L-4
    title: Instance model does not match declarative model
    description: >
      The instantiated system tree diverges from the declared AADL
      structure due to incorrect expansion, missing connections,
      or wrong property inheritance.
    severity: critical
    losses: [L-1, L-4]

  - id: H-4
    type: hazard
    links:
      - type: leads-to-loss
        target: L-4
    title: Serialized output does not match internal model
    description: >
      JSON, SVG, or text output represents a different model than
      what spar computed internally (serialization/rendering bug).
    severity: critical
    losses: [L-4]

  - id: H-5
    type: hazard
    links:
      - type: leads-to-loss
        target: L-1
      - type: leads-to-loss
        target: L-3
    title: Parser silently drops valid AADL constructs
    description: >
      The parser accepts input without error but silently omits valid
      AADL constructs from the CST, causing downstream analyses to
      operate on an incomplete model.
    severity: critical
    losses: [L-1, L-3]

  - id: H-6
    type: hazard
    links:
      - type: leads-to-loss
        target: L-1
    title: Property values incorrectly evaluated
    description: >
      Timing, memory, or deployment properties are parsed or evaluated
      to wrong numeric values, causing analyses to compute incorrect
      results (e.g., wrong period causes RMA to pass when it should fail).
    severity: critical
    losses: [L-1]

  - id: H-7
    type: hazard
    links:
      - type: leads-to-loss
        target: L-1
      - type: leads-to-loss
        target: L-4
    title: SysML v2 lowering produces semantically incorrect AADL
    description: >
      The SysML v2 to AADL lowering transformation produces AADL
      constructs that are syntactically valid but semantically wrong
      (e.g., wrong component category, lost property constraints,
      missing connections). The resulting AADL model passes all 21
      analysis passes but does not faithfully represent the original
      SysML v2 design intent.
    severity: critical
    losses: [L-1, L-4]

  - id: H-8
    type: hazard
    links:
      - type: leads-to-loss
        target: L-1
      - type: leads-to-loss
        target: L-3
    title: Verification pipeline provides false assurance
    description: >
      The Bazel-based verification pipeline (Verus, Lean4, WASM component
      rules) reports success when verification was not actually performed
      (e.g., tool not installed, fallback to no-op, cached stale result).
      Engineers believe generated code is formally verified when it is not.
    severity: critical
    losses: [L-1, L-3]

  # ══════════════════════════════════════════════════════════════════════
  # STEP 1c: System-Level Constraints
  # ══════════════════════════════════════════════════════════════════════

  - id: SC-1
    type: system-constraint
    links:
      - type: prevents
        target: H-1
    title: No false negatives on safety analyses
    description: >
      Spar must detect all genuine architectural defects for which it
      has implemented analysis passes. Coverage gaps must be documented.
    spec-baseline: AS5506C
    hazards: [H-1]

  - id: SC-2
    type: system-constraint
    links:
      - type: prevents
        target: H-2
    title: Minimize false positives
    description: >
      Spar should not report defects that do not exist. When uncertain,
      spar should clearly indicate the confidence level (info vs warning
      vs error severity).
    hazards: [H-2]

  - id: SC-3
    type: system-constraint
    links:
      - type: prevents
        target: H-3
    title: Instance model fidelity
    description: >
      The instance model must faithfully represent the declared AADL
      structure. Every subcomponent, connection, mode, flow, and property
      in the declarative model must appear in the instance model.
    hazards: [H-3]

  - id: SC-4
    type: system-constraint
    links:
      - type: prevents
        target: H-4
    title: Output fidelity
    description: >
      All serialized outputs (JSON, SVG, text) must accurately represent
      the internal computed model. Round-trip deserialization must produce
      equivalent data.
    hazards: [H-4]

  - id: SC-5
    type: system-constraint
    links:
      - type: prevents
        target: H-5
    title: Parser completeness
    description: >
      The parser must produce CST nodes for all valid AADL v2.2 constructs.
      Unrecognized constructs must produce error diagnostics, never silent
      omission.
    hazards: [H-5]

  - id: SC-6
    type: system-constraint
    links:
      - type: prevents
        target: H-6
    title: Property evaluation correctness
    description: >
      Property values must be evaluated with correct units, arithmetic,
      defaults, and inheritance chains. Unit conversion factors must match
      the AS5506 standard.
    hazards: [H-6]

  - id: SC-7
    type: system-constraint
    links:
      - type: prevents
        target: H-7
    title: SysML v2 lowering semantic fidelity
    description: >
      The SysML v2 to AADL lowering must faithfully preserve the design
      intent of the original SysML v2 model. Component categories, port
      directions, connection topology, property values, and constraint
      semantics must be correctly mapped. Unhandled SysML v2 constructs
      must produce diagnostics, not be silently dropped.
    hazards: [H-7]

  - id: SC-8
    type: system-constraint
    links:
      - type: prevents
        target: H-8
    title: Verification pipeline integrity
    description: >
      The Bazel verification pipeline must fail loudly when verification
      tools (Verus, Lean4, wasm-tools) are unavailable or produce errors.
      A green build must mean verification was actually performed, not
      that verification was skipped.
    hazards: [H-8]

  # ══════════════════════════════════════════════════════════════════════
  # STEP 2: Control Structure
  # ══════════════════════════════════════════════════════════════════════

  - id: CTRL-ENGINEER
    type: controller
    title: AADL Engineer
    controller-type: human
    process-model:
      - Believes the AADL model is syntactically and semantically correct
      - Believes spar will detect architectural defects
      - May not know all AADL legality rules
      - Relies on spar diagnostics to guide model corrections

  - id: CTRL-REVIEWER
    type: controller
    title: Safety Reviewer
    controller-type: human
    process-model:
      - Believes spar analysis output is complete and correct
      - Uses analysis results as evidence for certification
      - May not independently verify spar results
      - Assumes spar coverage matches documented capability

  - id: CTRL-PARSER
    type: controller
    title: Parser Controller (spar-parser + spar-syntax)
    controller-type: automated
    source-file: crates/spar-parser/src/lib.rs
    process-model:
      - Token stream represents complete input
      - Grammar rules cover all AADL v2.2 productions
      - Error recovery preserves unparsed tokens

  - id: CTRL-MODEL
    type: controller
    title: Model Builder (spar-hir-def)
    controller-type: automated
    source-file: crates/spar-hir-def/src/item_tree/lower.rs
    process-model:
      - CST is complete (all valid constructs present)
      - Lowering handles all SyntaxKind variants
      - Property expressions are correctly typed
      - Name resolution finds all cross-file references

  - id: CTRL-INSTANCE
    type: controller
    title: Instance Builder (spar-hir-def::instance)
    controller-type: automated
    source-file: crates/spar-hir-def/src/instance.rs
    process-model:
      - Declarative model is complete and correct
      - Classifier references resolve to valid types
      - Recursive expansion terminates
      - Array dimensions are finite positive integers

  - id: CTRL-ANALYSIS
    type: controller
    title: Analysis Engine (spar-analysis)
    controller-type: automated
    source-file: crates/spar-analysis/src/lib.rs
    process-model:
      - Instance model faithfully represents the architecture
      - Property values are correctly evaluated
      - All relevant analysis passes are registered and run
      - Diagnostic severity correctly reflects defect impact

  - id: CTRL-OUTPUT
    type: controller
    title: Output Controller (spar-cli, spar-wasm)
    controller-type: automated
    source-file: crates/spar-cli/src/main.rs
    process-model:
      - Analysis diagnostics are complete
      - Serialization preserves all fields
      - Format conversion (JSON, SVG, text) is lossless for the domain

  - id: CTRL-SYSML2
    type: controller
    title: SysML v2 Lowering Controller (spar-sysml2)
    controller-type: automated
    source-file: crates/spar-sysml2/src/lower.rs
    process-model:
      - SysML v2 CST is complete (all valid constructs parsed)
      - SEI mapping rules cover all SysML v2 construct types
      - Category inference heuristics produce correct AADL categories
      - Property semantics are preserved across the SysML/AADL boundary
      - Unhandled SysML v2 constructs are rare and non-safety-relevant

  - id: CTRL-CODEGEN
    type: controller
    title: Code Generator (spar-codegen)
    controller-type: automated
    source-file: crates/spar-codegen/src/workspace_gen.rs
    process-model:
      - AADL instance model is correct and complete
      - Generated Bazel rules reference valid tool paths
      - Verification rules (Verus, Lean4) produce definitive pass/fail
      - WASM component packaging preserves interface contracts

  # ── Controlled Processes ───────────────────────────────────────────────

  - id: CP-SOURCE
    type: controlled-process
    title: AADL Source Files
    description: The .aadl input files written by engineers

  - id: CP-MODEL
    type: controlled-process
    title: Internal AADL Model (ItemTree + Instance)
    description: The in-memory representation of the AADL architecture

  - id: CP-DIAGNOSTICS
    type: controlled-process
    title: Analysis Diagnostics
    description: The list of errors, warnings, and info diagnostics produced

  - id: CP-DECISIONS
    type: controlled-process
    title: Architecture Decisions
    description: Downstream design decisions informed by spar analysis

  # ── Control Actions ────────────────────────────────────────────────────

  - id: CA-PARSE
    type: control-action
    links:
      - type: issued-by
        target: CTRL-PARSER
      - type: acts-on
        target: CP-MODEL
    title: Parse AADL source
    action: Transform source text into concrete syntax tree
    source: CTRL-PARSER
    target: CP-MODEL

  - id: CA-LOWER
    type: control-action
    links:
      - type: issued-by
        target: CTRL-MODEL
      - type: acts-on
        target: CP-MODEL
    title: Lower CST to ItemTree
    action: Convert syntax tree nodes to typed HIR items
    source: CTRL-MODEL
    target: CP-MODEL

  - id: CA-INSTANTIATE
    type: control-action
    links:
      - type: issued-by
        target: CTRL-INSTANCE
      - type: acts-on
        target: CP-MODEL
    title: Instantiate system
    action: Recursively expand root implementation into instance tree
    source: CTRL-INSTANCE
    target: CP-MODEL

  - id: CA-ANALYZE
    type: control-action
    links:
      - type: issued-by
        target: CTRL-ANALYSIS
      - type: acts-on
        target: CP-DIAGNOSTICS
    title: Run analysis passes
    action: Execute registered analyses against instance model
    source: CTRL-ANALYSIS
    target: CP-DIAGNOSTICS

  - id: CA-REPORT
    type: control-action
    links:
      - type: issued-by
        target: CTRL-OUTPUT
      - type: acts-on
        target: CP-DECISIONS
    title: Report results
    action: Format and output analysis diagnostics
    source: CTRL-OUTPUT
    target: CP-DECISIONS

  - id: CA-REVIEW
    type: control-action
    links:
      - type: issued-by
        target: CTRL-REVIEWER
      - type: acts-on
        target: CP-DECISIONS
    title: Review and approve architecture
    action: Evaluate analysis output and decide on architecture approval
    source: CTRL-REVIEWER
    target: CP-DECISIONS

  - id: CA-SYSML2-LOWER
    type: control-action
    links:
      - type: issued-by
        target: CTRL-SYSML2
      - type: acts-on
        target: CP-MODEL
    title: Lower SysML v2 to AADL
    action: Transform SysML v2 CST into AADL ItemTree using SEI mapping rules
    source: CTRL-SYSML2
    target: CP-MODEL

  - id: CA-CODEGEN
    type: control-action
    links:
      - type: issued-by
        target: CTRL-CODEGEN
      - type: acts-on
        target: CP-DECISIONS
    title: Generate code and verification pipeline
    action: >
      Generate Rust crate skeletons, WIT interfaces, and Bazel BUILD files
      with verification rules from the AADL instance model
    source: CTRL-CODEGEN
    target: CP-DECISIONS

  # ══════════════════════════════════════════════════════════════════════
  # STEP 3: Unsafe Control Actions
  # ══════════════════════════════════════════════════════════════════════

  # ── Parser UCAs ────────────────────────────────────────────────────────

  - id: UCA-1
    type: uca
    links:
      - type: issued-by
        target: CTRL-PARSER
      - type: leads-to-hazard
        target: H-5
    title: Parser silently drops construct
    uca-type: not-providing
    context: >
      When AADL source contains a valid construct (e.g., annex subclause,
      prototype binding, call sequence) that the parser does not recognize.
    rationale: >
      Missing CST node means the construct is invisible to all downstream
      processing. No diagnostic is emitted, so the engineer believes the
      model is complete.
    controller: CTRL-PARSER
    hazards: [H-5]

  - id: UCA-2
    type: uca
    links:
      - type: issued-by
        target: CTRL-PARSER
      - type: leads-to-hazard
        target: H-1
      - type: leads-to-hazard
        target: H-5
    title: Parser accepts invalid AADL without error
    uca-type: providing
    context: >
      When the source contains a syntax error but the parser's error
      recovery consumes it without emitting a diagnostic.
    rationale: >
      Engineer believes the model is valid when it is not. Downstream
      analyses may produce incorrect results on a malformed model.
    controller: CTRL-PARSER
    hazards: [H-1, H-5]

  # ── Model Builder UCAs ────────────────────────────────────────────────

  - id: UCA-3
    type: uca
    links:
      - type: issued-by
        target: CTRL-MODEL
      - type: leads-to-hazard
        target: H-1
      - type: leads-to-hazard
        target: H-3
    title: Lowering omits CST node
    uca-type: not-providing
    context: >
      When the CST contains a valid node (e.g., property association,
      mode transition trigger, connection in_modes) but the lowering
      code does not handle that SyntaxKind.
    rationale: >
      ItemTree is incomplete. Analyses that depend on the missing data
      will produce false negatives.
    controller: CTRL-MODEL
    hazards: [H-1, H-3]

  - id: UCA-4
    type: uca
    links:
      - type: issued-by
        target: CTRL-MODEL
      - type: leads-to-hazard
        target: H-6
    title: Lowering assigns wrong property value
    uca-type: providing
    context: >
      When a property expression is lowered with incorrect unit conversion,
      wrong numeric parsing, or misidentified property type.
    rationale: >
      Scheduling analysis may use wrong period/deadline values. Resource
      budget may use wrong memory sizes.
    controller: CTRL-MODEL
    hazards: [H-6]

  - id: UCA-5
    type: uca
    links:
      - type: issued-by
        target: CTRL-MODEL
      - type: leads-to-hazard
        target: H-3
    title: Name resolution returns wrong classifier
    uca-type: providing
    context: >
      When two packages define types with similar names and the resolver
      picks the wrong one due to case-insensitive matching or import order.
    rationale: >
      Subcomponent instantiates the wrong type. Connection type checking
      passes when it should fail.
    controller: CTRL-MODEL
    hazards: [H-3]

  # ── Instance Builder UCAs ─────────────────────────────────────────────

  - id: UCA-6
    type: uca
    links:
      - type: issued-by
        target: CTRL-INSTANCE
      - type: leads-to-hazard
        target: H-3
    title: Instance expansion misses subcomponent
    uca-type: not-providing
    context: >
      When a component implementation has subcomponents filtered by modes
      and the instance builder incorrectly filters them out in the
      default (non-modal) expansion.
    rationale: >
      Missing subcomponent means missing connections and missing analyses.
      An entire subsystem could be invisible.
    controller: CTRL-INSTANCE
    hazards: [H-3]

  - id: UCA-7
    type: uca
    links:
      - type: issued-by
        target: CTRL-INSTANCE
      - type: leads-to-hazard
        target: H-3
      - type: leads-to-hazard
        target: H-1
    title: Array expansion produces wrong count
    uca-type: providing
    context: >
      When array dimension expression evaluation produces wrong N,
      or when array indexing in connection patterns is off-by-one.
    rationale: >
      Too few instances: missing redundancy paths. Too many: phantom
      components consume scheduling/resource budgets incorrectly.
    controller: CTRL-INSTANCE
    hazards: [H-3, H-1]

  - id: UCA-8
    type: uca
    links:
      - type: issued-by
        target: CTRL-INSTANCE
      - type: leads-to-hazard
        target: H-3
      - type: leads-to-hazard
        target: H-1
    title: Connection tracing produces wrong endpoint
    uca-type: providing
    context: >
      When multi-level connection tracing (up/down patterns) follows
      the wrong feature in a feature group or resolves to a feature
      in the wrong subcomponent.
    rationale: >
      Connectivity analysis passes (no unconnected ports) but the actual
      data flow path is wrong. Latency analysis computes wrong path.
    controller: CTRL-INSTANCE
    hazards: [H-3, H-1]

  - id: UCA-9
    type: uca
    links:
      - type: issued-by
        target: CTRL-INSTANCE
      - type: leads-to-hazard
        target: H-3
    title: Instance builder enters infinite recursion
    uca-type: stopped-too-soon
    context: >
      When a component implementation contains a subcomponent whose
      classifier directly or indirectly references the parent
      (circular containment).
    rationale: >
      Stack overflow crashes spar. No analysis output is produced.
      Engineer may not understand the error.
    controller: CTRL-INSTANCE
    hazards: [H-3]

  # ── Analysis Engine UCAs ──────────────────────────────────────────────

  - id: UCA-10
    type: uca
    links:
      - type: issued-by
        target: CTRL-ANALYSIS
      - type: leads-to-hazard
        target: H-1
    title: Analysis not registered
    uca-type: not-providing
    context: >
      When a relevant analysis pass exists but is not registered with
      the AnalysisRunner for the current invocation (e.g., ARINC 653
      analysis exists but is not added when analyzing a partitioned system).
    rationale: >
      Entire class of defects goes undetected. Engineer believes the
      model was fully analyzed.
    controller: CTRL-ANALYSIS
    hazards: [H-1]

  - id: UCA-11
    type: uca
    links:
      - type: issued-by
        target: CTRL-ANALYSIS
      - type: leads-to-hazard
        target: H-1
      - type: leads-to-hazard
        target: H-6
    title: Analysis uses wrong property value
    uca-type: providing
    context: >
      When the analysis reads a property from the instance model but
      the property was incorrectly inherited, defaulted, or unit-converted.
    rationale: >
      RMA with wrong period: schedulability check is meaningless.
      Resource budget with wrong memory size: budget check is wrong.
    controller: CTRL-ANALYSIS
    hazards: [H-1, H-6]

  - id: UCA-12
    type: uca
    links:
      - type: issued-by
        target: CTRL-ANALYSIS
      - type: leads-to-hazard
        target: H-1
    title: Analysis emits wrong severity
    uca-type: providing
    context: >
      When a genuine safety-critical defect (e.g., CPU utilization > 100%)
      is reported as info or warning instead of error.
    rationale: >
      Engineer or reviewer may dismiss the diagnostic. The defect
      persists in the approved architecture.
    controller: CTRL-ANALYSIS
    hazards: [H-1]

  - id: UCA-13
    type: uca
    links:
      - type: issued-by
        target: CTRL-ANALYSIS
      - type: leads-to-hazard
        target: H-2
    title: Analysis produces false positive
    uca-type: providing
    context: >
      When the analysis reports a defect that does not exist because
      it does not account for modal filtering, property overrides,
      or correct inheritance.
    rationale: >
      Wastes engineering effort. Repeated false positives erode trust.
    controller: CTRL-ANALYSIS
    hazards: [H-2]

  # ── Output Controller UCAs ────────────────────────────────────────────

  - id: UCA-14
    type: uca
    links:
      - type: issued-by
        target: CTRL-OUTPUT
      - type: leads-to-hazard
        target: H-4
    title: JSON serialization drops field
    uca-type: not-providing
    context: >
      When a spar-hir type gains a new field but the serde derive
      does not include it (e.g., field added to struct but not to
      the serializable projection).
    rationale: >
      Downstream consumers (rivet AADL adapter) see incomplete data.
      Architecture documentation is incomplete.
    controller: CTRL-OUTPUT
    hazards: [H-4]

  - id: UCA-15
    type: uca
    links:
      - type: issued-by
        target: CTRL-OUTPUT
      - type: leads-to-hazard
        target: H-4
    title: SVG rendering misrepresents topology
    uca-type: providing
    context: >
      When the graph builder omits connections, misplaces nodes, or
      renders wrong port labels in the SVG diagram.
    rationale: >
      Visual architecture documentation does not match the actual model.
      Reviewer makes decisions based on incorrect diagram.
    controller: CTRL-OUTPUT
    hazards: [H-4]

  - id: UCA-16
    type: uca
    links:
      - type: issued-by
        target: CTRL-OUTPUT
      - type: leads-to-hazard
        target: H-1
    title: Diagnostic output suppresses errors
    uca-type: not-providing
    context: >
      When the CLI or WASM output formatter filters, truncates, or
      fails to transmit error-severity diagnostics to the user.
    rationale: >
      Critical defects are computed but never shown to the engineer.
    controller: CTRL-OUTPUT
    hazards: [H-1]

  # ── SysML v2 Lowering UCAs ────────────────────────────────────────────

  - id: UCA-17
    type: uca
    links:
      - type: issued-by
        target: CTRL-SYSML2
      - type: leads-to-hazard
        target: H-7
    title: SysML v2 lowering silently drops construct
    uca-type: not-providing
    context: >
      When the SysML v2 source contains a valid construct (e.g., flow
      definition, view def, analysis case, occurrence def) that the
      lower_node wildcard arm silently ignores via `_ => {}`.
    rationale: >
      The construct is invisible to all downstream AADL processing. No
      diagnostic is emitted, so the engineer believes the lowered model
      is complete. If the dropped construct carried safety-critical
      semantics (e.g., a timing constraint or allocation), the resulting
      AADL model is incomplete.
    controller: CTRL-SYSML2
    hazards: [H-7]

  - id: UCA-18
    type: uca
    links:
      - type: issued-by
        target: CTRL-SYSML2
      - type: leads-to-hazard
        target: H-7
      - type: leads-to-hazard
        target: H-1
    title: SysML v2 lowering assigns wrong component category
    uca-type: providing
    context: >
      When the infer_category heuristic misclassifies a part def
      (e.g., a software process as a system, or a thread group as a
      process) because the heuristic only checks for action/state
      usages in the body.
    rationale: >
      Wrong category causes wrong analysis pass selection. A thread
      classified as a system is never scheduled. A process classified
      as a system does not get connectivity checks on internal ports.
      Scheduling analysis produces no results (false negative).
    controller: CTRL-SYSML2
    hazards: [H-7, H-1]

  - id: UCA-19
    type: uca
    links:
      - type: issued-by
        target: CTRL-SYSML2
      - type: leads-to-hazard
        target: H-7
      - type: leads-to-hazard
        target: H-6
    title: SysML v2 property semantics lost in lowering
    uca-type: providing
    context: >
      When a SysML v2 constraint usage or attribute usage carries timing
      or resource semantics but is lowered to an Opaque PropertyExpr
      that downstream AADL analyses cannot interpret.
    rationale: >
      The property exists in the AADL model but has no typed value.
      Scheduling analysis skips it (no typed Period). The engineer
      believes timing constraints from SysML v2 are being checked
      when they are not.
    controller: CTRL-SYSML2
    hazards: [H-7, H-6]

  - id: UCA-20
    type: uca
    links:
      - type: issued-by
        target: CTRL-SYSML2
      - type: leads-to-hazard
        target: H-7
      - type: leads-to-hazard
        target: H-3
    title: Subcomponent category hardcoded to System
    uca-type: providing
    context: >
      When lower_part_usage_to_subcomponent and lower_ref_usage_to_subcomponent
      always set category to ComponentCategory::System regardless of the
      referenced type's actual category in the SysML v2 model.
    rationale: >
      A process subcomponent classified as system will not have its
      threads scheduled. A bus subcomponent classified as system will
      not participate in binding analysis. The wrong category propagates
      through instantiation to all downstream analyses.
    controller: CTRL-SYSML2
    hazards: [H-7, H-3]

  # ── Codegen / Verification Pipeline UCAs ────────────────────────────

  - id: UCA-21
    type: uca
    links:
      - type: issued-by
        target: CTRL-CODEGEN
      - type: leads-to-hazard
        target: H-8
    title: Verification rule silently passes when tool missing
    uca-type: not-providing
    context: >
      When the Bazel verus_verify or lean_verify rule falls back to a
      PATH lookup for the tool binary, and the binary is not installed,
      the shell command may produce a non-zero exit but Bazel caching
      or error handling could mask the failure in certain configurations.
    rationale: >
      Engineers see a cached green build and believe verification was
      performed. The generated code ships without formal verification.
      This is a false assurance hazard.
    controller: CTRL-CODEGEN
    hazards: [H-8]

  - id: UCA-22
    type: uca
    links:
      - type: issued-by
        target: CTRL-CODEGEN
      - type: leads-to-hazard
        target: H-8
    title: Generated BUILD.bazel omits verification targets
    uca-type: not-providing
    context: >
      When workspace_gen.rs generates per-crate BUILD.bazel files that
      include rust_library and wasm_component targets but do not include
      verus_verify or lean_verify targets for the generated code.
    rationale: >
      The generated project builds and tests pass, but no formal
      verification is ever invoked. The verification pipeline exists
      in the workspace root but is not wired to the generated crates.
    controller: CTRL-CODEGEN
    hazards: [H-8]

  # ══════════════════════════════════════════════════════════════════════
  # STEP 3b: Controller Constraints
  # ══════════════════════════════════════════════════════════════════════

  - id: CC-1
    type: controller-constraint
    links:
      - type: constrains-controller
        target: CTRL-PARSER
      - type: inverts-uca
        target: UCA-1
      - type: inverts-uca
        target: UCA-2
      - type: prevents
        target: H-5
    title: Parser must emit diagnostic for unrecognized constructs
    constraint: >
      The parser must produce an error diagnostic for any token sequence
      it cannot match to an AADL production. Silent consumption of
      tokens without CST node creation is prohibited.
    controller: CTRL-PARSER
    ucas: [UCA-1, UCA-2]
    hazards: [H-5]

  - id: CC-2
    type: controller-constraint
    links:
      - type: constrains-controller
        target: CTRL-MODEL
      - type: inverts-uca
        target: UCA-3
      - type: prevents
        target: H-3
    title: Lowering must handle all SyntaxKind variants
    constraint: >
      The CST-to-ItemTree lowering must have a match arm for every
      SyntaxKind that represents a semantic AADL construct. Unhandled
      variants must emit a warning diagnostic.
    controller: CTRL-MODEL
    ucas: [UCA-3]
    hazards: [H-3]

  - id: CC-3
    type: controller-constraint
    links:
      - type: constrains-controller
        target: CTRL-MODEL
      - type: inverts-uca
        target: UCA-4
      - type: prevents
        target: H-6
    title: Property evaluation must use standard unit factors
    constraint: >
      Unit conversion factors must match AS5506 Appendix A.
      Property values must be validated against their declared type.
    controller: CTRL-MODEL
    ucas: [UCA-4]
    hazards: [H-6]

  - id: CC-4
    type: controller-constraint
    links:
      - type: constrains-controller
        target: CTRL-MODEL
      - type: inverts-uca
        target: UCA-5
      - type: prevents
        target: H-3
    title: Resolver must handle ambiguous names deterministically
    constraint: >
      When multiple classifiers match a reference, the resolver must
      prefer the local package, then follow import order, and emit
      a warning for ambiguous resolution.
    controller: CTRL-MODEL
    ucas: [UCA-5]
    hazards: [H-3]

  - id: CC-5
    type: controller-constraint
    links:
      - type: constrains-controller
        target: CTRL-INSTANCE
      - type: inverts-uca
        target: UCA-6
      - type: prevents
        target: H-3
    title: Instance builder must include all non-modal subcomponents
    constraint: >
      Subcomponents without in_modes filtering must always be instantiated.
      Modal subcomponents must be instantiated in all modes (with mode
      membership tracking).
    controller: CTRL-INSTANCE
    ucas: [UCA-6]
    hazards: [H-3]

  - id: CC-6
    type: controller-constraint
    links:
      - type: constrains-controller
        target: CTRL-INSTANCE
      - type: inverts-uca
        target: UCA-7
      - type: prevents
        target: H-3
    title: Array dimensions must be validated positive
    constraint: >
      Array dimension expressions must evaluate to positive integers.
      Array index patterns in connections must be bounds-checked.
    controller: CTRL-INSTANCE
    ucas: [UCA-7]
    hazards: [H-3]

  - id: CC-7
    type: controller-constraint
    links:
      - type: constrains-controller
        target: CTRL-INSTANCE
      - type: inverts-uca
        target: UCA-8
      - type: prevents
        target: H-3
    title: Connection tracing must verify endpoints
    constraint: >
      After multi-level connection tracing, both endpoints must resolve
      to valid feature instances. Unresolved endpoints must produce
      diagnostics.
    controller: CTRL-INSTANCE
    ucas: [UCA-8]
    hazards: [H-3]

  - id: CC-8
    type: controller-constraint
    links:
      - type: constrains-controller
        target: CTRL-INSTANCE
      - type: inverts-uca
        target: UCA-9
      - type: prevents
        target: H-3
    title: Instance builder must detect circular containment
    constraint: >
      Before recursive expansion, check for cycles in the classifier
      reference graph. Emit an error and stop expansion if a cycle
      is detected.
    controller: CTRL-INSTANCE
    ucas: [UCA-9]
    hazards: [H-3]

  - id: CC-9
    type: controller-constraint
    links:
      - type: constrains-controller
        target: CTRL-ANALYSIS
      - type: inverts-uca
        target: UCA-10
      - type: prevents
        target: H-1
    title: All safety analyses must be registered by default
    constraint: >
      The AnalysisRunner must register all implemented analysis passes
      by default. Selective registration is allowed only via explicit
      user opt-out.
    controller: CTRL-ANALYSIS
    ucas: [UCA-10]
    hazards: [H-1]

  - id: CC-10
    type: controller-constraint
    links:
      - type: constrains-controller
        target: CTRL-ANALYSIS
      - type: inverts-uca
        target: UCA-11
      - type: prevents
        target: H-1
      - type: prevents
        target: H-6
    title: Analyses must read properties through validated accessors
    constraint: >
      Analysis passes must not directly interpret raw property strings.
      All property access must go through typed accessor functions that
      perform unit conversion and type validation.
    controller: CTRL-ANALYSIS
    ucas: [UCA-11]
    hazards: [H-1, H-6]

  - id: CC-11
    type: controller-constraint
    links:
      - type: constrains-controller
        target: CTRL-ANALYSIS
      - type: inverts-uca
        target: UCA-12
      - type: prevents
        target: H-1
    title: Severity assignment must follow documented criteria
    constraint: >
      Error = confirmed standard violation or guaranteed runtime failure.
      Warning = likely defect or incomplete specification.
      Info = style suggestion or optional improvement.
    controller: CTRL-ANALYSIS
    ucas: [UCA-12]
    hazards: [H-1]

  - id: CC-12
    type: controller-constraint
    links:
      - type: constrains-controller
        target: CTRL-ANALYSIS
      - type: inverts-uca
        target: UCA-13
      - type: prevents
        target: H-2
    title: Analyses must account for modes and property overrides
    constraint: >
      Before reporting a defect, analyses must check whether the condition
      is filtered by modes or overridden by property associations at a
      more specific level.
    controller: CTRL-ANALYSIS
    ucas: [UCA-13]
    hazards: [H-2]

  - id: CC-13
    type: controller-constraint
    links:
      - type: constrains-controller
        target: CTRL-OUTPUT
      - type: inverts-uca
        target: UCA-14
      - type: prevents
        target: H-4
    title: Serialization must include all public fields
    constraint: >
      Serde derives must be present on all public types. New fields
      added to structs must be included in serialization. Integration
      tests must verify round-trip fidelity.
    controller: CTRL-OUTPUT
    ucas: [UCA-14]
    hazards: [H-4]

  - id: CC-14
    type: controller-constraint
    links:
      - type: constrains-controller
        target: CTRL-OUTPUT
      - type: inverts-uca
        target: UCA-16
      - type: prevents
        target: H-1
    title: Output must not filter error diagnostics
    constraint: >
      The output formatter must transmit all diagnostics regardless
      of severity. Filtering is only allowed via explicit user flags
      (e.g., --severity-min warning).
    controller: CTRL-OUTPUT
    ucas: [UCA-16]
    hazards: [H-1]

  - id: CC-15
    type: controller-constraint
    links:
      - type: constrains-controller
        target: CTRL-SYSML2
      - type: inverts-uca
        target: UCA-17
      - type: prevents
        target: H-7
    title: SysML v2 lowering must emit diagnostic for unhandled constructs
    constraint: >
      The lower_node function must not have a silent wildcard arm. Every
      SysML v2 SyntaxKind not explicitly handled must produce a warning
      diagnostic "unhandled SysML v2 construct: {kind}". This mirrors
      the AADL lowering constraint (CC-2).
    controller: CTRL-SYSML2
    ucas: [UCA-17]
    hazards: [H-7]

  - id: CC-16
    type: controller-constraint
    links:
      - type: constrains-controller
        target: CTRL-SYSML2
      - type: inverts-uca
        target: UCA-18
      - type: inverts-uca
        target: UCA-20
      - type: prevents
        target: H-7
    title: Category inference must be validated against type definition
    constraint: >
      After lowering, the inferred category of a part def should be
      validated against the features present. If the part has thread-like
      properties (Period, Dispatch_Protocol) it must not be classified
      as system. A mapping coverage test must verify all category
      inference paths.
    controller: CTRL-SYSML2
    ucas: [UCA-18, UCA-20]
    hazards: [H-7]

  - id: CC-17
    type: controller-constraint
    links:
      - type: constrains-controller
        target: CTRL-SYSML2
      - type: inverts-uca
        target: UCA-19
      - type: prevents
        target: H-7
      - type: prevents
        target: H-6
    title: SysML v2 constraint values must produce typed PropertyExpr
    constraint: >
      When lowering SysML v2 attribute or constraint usages that carry
      numeric values with units (e.g., period = 10 ms), the lowering
      must produce a typed PropertyExpr (IntegerLit with unit), not an
      Opaque expression. Opaque is acceptable only for genuinely unparseable
      expressions.
    controller: CTRL-SYSML2
    ucas: [UCA-19]
    hazards: [H-7, H-6]

  - id: CC-18
    type: controller-constraint
    links:
      - type: constrains-controller
        target: CTRL-CODEGEN
      - type: inverts-uca
        target: UCA-21
      - type: prevents
        target: H-8
    title: Verification rules must fail on missing tools
    constraint: >
      Bazel verification rules (verus_verify, lean_verify) must explicitly
      check for tool availability and produce a clear error message if the
      tool binary is not found. The rule must not produce a cached success
      artifact when verification was not performed.
    controller: CTRL-CODEGEN
    ucas: [UCA-21]
    hazards: [H-8]

  - id: CC-19
    type: controller-constraint
    links:
      - type: constrains-controller
        target: CTRL-CODEGEN
      - type: inverts-uca
        target: UCA-22
      - type: prevents
        target: H-8
    title: Generated crates must include verification targets
    constraint: >
      The code generator must produce verus_verify and/or lean_verify
      targets in per-crate BUILD.bazel files when verification source
      files are present. An integration test must verify that generated
      BUILD.bazel files contain verification targets.
    controller: CTRL-CODEGEN
    ucas: [UCA-22]
    hazards: [H-8]

  # ══════════════════════════════════════════════════════════════════════
  # STEP 4: Loss Scenarios
  # ══════════════════════════════════════════════════════════════════════

  - id: LS-1
    type: loss-scenario
    links:
      - type: caused-by-uca
        target: UCA-1
      - type: leads-to-hazard
        target: H-5
      - type: leads-to-hazard
        target: H-1
    title: Annex subclause silently dropped
    scenario-type: inadequate-control-algorithm
    description: >
      The parser encounters an annex subclause (e.g., EMV2 error model
      within a component) but the annex parsing code returns None instead
      of an error. The CST has no node for the annex. The model builder
      never sees the error model. EMV2 fault tree analysis finds no
      annotations and reports "no error model" (info). The actual error
      propagation paths are never checked.
    causal-factors:
      - spar-annex returns None for unrecognized annex names
      - No diagnostic emitted for unparsed annex content
      - EMV2 analysis treats missing annotations as "not applicable"
    uca: [UCA-1]
    hazards: [H-5, H-1]

  - id: LS-2
    type: loss-scenario
    links:
      - type: caused-by-uca
        target: UCA-4
      - type: caused-by-uca
        target: UCA-11
      - type: leads-to-hazard
        target: H-6
      - type: leads-to-hazard
        target: H-1
    title: Unit conversion factor wrong for time property
    scenario-type: inadequate-process-model
    description: >
      A property like Period => 10 ms is lowered to a PropertyExpr with
      the wrong conversion factor (e.g., factor of 1000 instead of
      1_000_000 for ms-to-ps). The scheduling analysis reads Period as
      10_000 ps instead of 10_000_000_000 ps. RMA computes utilization
      with a period 1000x smaller than actual, reporting a false pass.
    causal-factors:
      - Unit conversion table in standard_properties.rs has wrong factor
      - No cross-check against known good values in tests
      - RMA formula does not sanity-check period magnitude
    uca: [UCA-4, UCA-11]
    hazards: [H-6, H-1]

  - id: LS-3
    type: loss-scenario
    links:
      - type: caused-by-uca
        target: UCA-9
      - type: leads-to-hazard
        target: H-3
    title: Recursive instantiation overflow
    scenario-type: controller-failure
    description: >
      An AADL model contains A.impl with subcomponent b: B, and B.impl
      with subcomponent a: A (mutual recursion). The instance builder
      has no cycle detection. Expansion enters infinite recursion and
      crashes with stack overflow. No diagnostics are produced. The
      engineer sees only "process terminated" with no explanation.
    causal-factors:
      - No cycle detection in instantiation
      - No recursion depth limit
      - Crash produces no diagnostic
    uca: [UCA-9]
    hazards: [H-3]

  - id: LS-4
    type: loss-scenario
    links:
      - type: caused-by-uca
        target: UCA-8
      - type: leads-to-hazard
        target: H-3
      - type: leads-to-hazard
        target: H-1
    title: Connection tracing follows wrong feature group member
    scenario-type: inadequate-control-algorithm
    description: >
      A feature group FG contains ports A and B. A connection maps
      sub1.fg -> sub2.fg. During semantic connection tracing, the
      algorithm matches FG members by position instead of by name.
      If sub1's FG has members [A, B] and sub2's has [B, A] (due to
      inverse_of), the connections are crossed: sub1.fg.A connects
      to sub2.fg.B. Connectivity analysis passes because all ports
      are connected. But the actual data flow is wrong.
    causal-factors:
      - Feature group member matching by index instead of name
      - inverse_of handling reverses member order
      - Connectivity analysis checks presence, not correctness
    uca: [UCA-8]
    hazards: [H-3, H-1]

  - id: LS-5
    type: loss-scenario
    links:
      - type: caused-by-uca
        target: UCA-10
      - type: leads-to-hazard
        target: H-1
    title: Analysis pass not registered after code addition
    scenario-type: inadequate-control-algorithm
    description: >
      A developer adds a new analysis pass (e.g., classifier_match.rs)
      but forgets to register it in the AnalysisRunner::register_all()
      function. The analysis code compiles and its unit tests pass in
      isolation. But when spar runs on a real model, the new analysis
      never executes. Connection type mismatches go undetected.
    causal-factors:
      - Manual registration required (no automatic discovery)
      - Unit tests test the analysis in isolation, not via AnalysisRunner
      - No integration test verifying all analyses are registered
    uca: [UCA-10]
    hazards: [H-1]

  - id: LS-6
    type: loss-scenario
    links:
      - type: caused-by-uca
        target: UCA-14
      - type: leads-to-hazard
        target: H-4
    title: JSON drops new InstanceNode field
    scenario-type: inadequate-feedback
    description: >
      A developer adds array_index to InstanceNode but the serializable
      projection (used for JSON output) is a separate struct that was
      not updated. The internal model has array indices. The JSON output
      does not. Rivet's AADL adapter receives JSON without array info.
      Array components appear as duplicates with the same name.
    causal-factors:
      - Serializable projection is manually maintained separately
      - No compile-time check that projection matches source struct
      - No round-trip test comparing internal vs. serialized model
    uca: [UCA-14]
    hazards: [H-4]

  - id: LS-7
    type: loss-scenario
    links:
      - type: caused-by-uca
        target: UCA-11
      - type: leads-to-hazard
        target: H-1
    title: Modal property override not considered in analysis
    scenario-type: inadequate-process-model
    description: >
      A thread has Period => 20ms globally but Period => 5ms in mode
      HighRate. The scheduling analysis reads only the default period
      (20ms). In HighRate mode, the actual period is 5ms, causing 4x
      higher CPU utilization. RMA reports the system is schedulable
      because it used the 20ms period.
    causal-factors:
      - Analysis reads only default (non-modal) property values
      - Modal property associations not evaluated per-mode
      - No per-mode scheduling analysis
    uca: [UCA-11]
    hazards: [H-1]

  - id: LS-8
    type: loss-scenario
    links:
      - type: caused-by-uca
        target: UCA-13
      - type: leads-to-hazard
        target: H-2
      - type: leads-to-hazard
        target: H-1
    title: Engineer dismisses analysis due to repeated false positives
    scenario-type: inadequate-feedback
    description: >
      Spar's connectivity analysis reports "unconnected port" for ports
      that are intentionally unconnected (monitoring ports, debug ports).
      After seeing many such false positives, the engineer stops reading
      connectivity diagnostics. A genuine unconnected safety-critical
      port is then missed among the noise.
    causal-factors:
      - No way to mark intentionally unconnected ports
      - No severity differentiation between required and optional ports
      - Alert fatigue causes engineer to ignore diagnostics
    uca: [UCA-13]
    hazards: [H-2, H-1]

  - id: LS-9
    type: loss-scenario
    links:
      - type: caused-by-uca
        target: UCA-17
      - type: leads-to-hazard
        target: H-7
      - type: leads-to-hazard
        target: H-1
    title: SysML v2 flow definition silently dropped during lowering
    scenario-type: inadequate-control-algorithm
    description: >
      A SysML v2 model contains a `flow def` that specifies an end-to-end
      data path between ports. The lower_node function matches against
      known SyntaxKinds but `FLOW_DEF` is not handled -- it falls through
      to `_ => {}`. No AADL flow spec or end-to-end flow is created. The
      lowered AADL model has all the ports and connections but no flow
      declarations. Latency analysis reports "no flows defined" (info)
      instead of computing latency bounds. The engineer believes the
      SysML v2 flows were carried over.
    causal-factors:
      - lower_node wildcard silently drops unrecognized SyntaxKinds
      - No diagnostic emitted for unhandled constructs
      - Latency analysis treats missing flows as "not applicable"
    uca: [UCA-17]
    hazards: [H-7, H-1]

  - id: LS-10
    type: loss-scenario
    links:
      - type: caused-by-uca
        target: UCA-18
      - type: caused-by-uca
        target: UCA-20
      - type: leads-to-hazard
        target: H-7
      - type: leads-to-hazard
        target: H-1
    title: Part def misclassified as system instead of process
    scenario-type: inadequate-process-model
    description: >
      A SysML v2 part def represents a software process containing threads.
      The infer_category heuristic checks for action/state usages in the
      body but the threads are expressed as nested part usages (not actions).
      The part is classified as ComponentCategory::System. The AADL model
      has a system implementation with system subcomponents where it should
      have a process implementation with thread subcomponents. Scheduling
      analysis finds no threads on any processor and reports no issues.
      The actual thread set is never checked for schedulability.
    causal-factors:
      - Category heuristic only checks for action/state, not thread indicators
      - Subcomponent lowering hardcodes System category
      - No post-lowering validation of category consistency
    uca: [UCA-18, UCA-20]
    hazards: [H-7, H-1]

  - id: LS-11
    type: loss-scenario
    links:
      - type: caused-by-uca
        target: UCA-19
      - type: leads-to-hazard
        target: H-7
      - type: leads-to-hazard
        target: H-6
    title: SysML v2 timing constraint lowered as Opaque property
    scenario-type: inadequate-control-algorithm
    description: >
      A SysML v2 constraint usage `constraint timing : TimingConstraint`
      with `attribute period = 10 ms` is lowered via
      lower_constraint_usage_to_property which produces a PropertyExpr::Opaque
      string "TimingConstraint" instead of a typed IntegerLit with unit.
      The AADL model has a Timing_Properties::timing property with an
      opaque value. Scheduling analysis calls get_timing_property() which
      cannot parse the opaque string and returns None. The thread's period
      is treated as unspecified. No scheduling check is performed.
    causal-factors:
      - lower_constraint_usage_to_property uses type ref as value, not the actual constraint value
      - PropertyExpr::Opaque skips property validation (by design for AADL)
      - Scheduling analysis silently skips components without Period
    uca: [UCA-19]
    hazards: [H-7, H-6]

  - id: LS-12
    type: loss-scenario
    links:
      - type: caused-by-uca
        target: UCA-21
      - type: leads-to-hazard
        target: H-8
    title: Verus not installed but BUILD succeeds from cache
    scenario-type: inadequate-feedback
    description: >
      A developer generates code with `spar codegen`. The generated
      BUILD.bazel loads verus_verify rules. On first build, Verus is not
      installed and the rule fails. The developer installs Verus and runs
      the build -- it succeeds and the proof log is cached. Later, the
      developer modifies generated source but Bazel's dependency tracking
      does not detect the change (e.g., the file is outside the sandbox).
      The stale cached proof log is reused. The modified code is not
      re-verified but the build reports success.
    causal-factors:
      - Bazel caching can serve stale verification results if inputs are not hermetic
      - verus_verify rule uses run_shell which may not capture all inputs
      - No verification artifact freshness check
    uca: [UCA-21]
    hazards: [H-8]

  - id: LS-13
    type: loss-scenario
    links:
      - type: caused-by-uca
        target: UCA-22
      - type: leads-to-hazard
        target: H-8
    title: Generated crate has no verification targets
    scenario-type: inadequate-control-algorithm
    description: >
      The workspace_gen.rs generates per-crate BUILD.bazel files with
      rust_library, wasm_component, and rust_test targets. However, it does
      not generate verus_verify or lean_verify targets because the code
      generator does not know which files contain proof annotations. The
      workspace root BUILD.bazel loads the verification rules but no
      per-crate target uses them. Running `bazel test //...` executes
      all rust_test targets but no formal verification. Engineers believe
      the full pipeline ran because the workspace imports verification rules.
    causal-factors:
      - workspace_gen.rs only generates build/test targets, not verification targets
      - Root BUILD.bazel imports verification rules but they are unused
      - No integration test checks that verification targets exist per crate
    uca: [UCA-22]
    hazards: [H-8]