Skip to content

Commit 7f54297

Browse files
avrabeavrabe
authored
docs: deployment solver research, rivet artifacts, STPA, and implementation plan (#75)
docs: deployment solver research, rivet artifacts, STPA, and implementation plan
2 parents 137b29f + ada6b8d commit 7f54297

10 files changed

Lines changed: 4095 additions & 0 deletions

‎AGENTS.md‎

Lines changed: 112 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,112 @@
1+
<!-- Auto-generated by `rivet init --agents`. Re-run to update after artifact changes. -->
2+
# AGENTS.md — Rivet Project Instructions
3+
4+
> This file was generated by `rivet init --agents`. Re-run the command
5+
> any time artifacts change to keep this file current.
6+
7+
## Project Overview
8+
9+
This project uses **Rivet** for SDLC artifact traceability.
10+
- Config: `rivet.yaml`
11+
- Schemas: common, dev, aspice, stpa, aadl
12+
- Artifacts: 221 across 3 types
13+
- Validation: `rivet validate` (current status: 21 errors)
14+
15+
## Available Commands
16+
17+
| Command | Purpose | Example |
18+
|---------|---------|---------|
19+
| `rivet validate` | Check link integrity, coverage, required fields | `rivet validate --format json` |
20+
| `rivet list` | List artifacts with filters | `rivet list --type requirement --format json` |
21+
| `rivet stats` | Show artifact counts by type | `rivet stats --format json` |
22+
| `rivet add` | Create a new artifact | `rivet add -t requirement --title "..." --link "satisfies:SC-1"` |
23+
| `rivet link` | Add a link between artifacts | `rivet link SOURCE -t satisfies --target TARGET` |
24+
| `rivet serve` | Start the dashboard | `rivet serve --port 3000` |
25+
| `rivet export` | Generate HTML reports | `rivet export --format html --output ./dist` |
26+
| `rivet impact` | Show change impact | `rivet impact --since HEAD~1` |
27+
| `rivet coverage` | Show traceability coverage | `rivet coverage --format json` |
28+
| `rivet diff` | Compare artifact versions | `rivet diff --base path/old --head path/new` |
29+
30+
## Artifact Types
31+
32+
| Type | Count | Description |
33+
|------|------:|-------------|
34+
| `design-decision` | 46 | An architectural or design decision with rationale |
35+
| `feature` | 90 | A user-visible capability or feature |
36+
| `requirement` | 85 | A functional or non-functional requirement |
37+
| `aadl-analysis-result` | 0 | Output of a spar analysis pass |
38+
| `aadl-component` | 0 | AADL component type or implementation imported from spar |
39+
| `aadl-flow` | 0 | End-to-end flow with latency bounds |
40+
| `aadl-tool` | 0 | An AADL ecosystem tool — captures what it does, what makes it unique, and what capabilities spar could adopt from it. |
41+
| `control-action` | 0 | An action issued by a controller to a controlled process or another controller. |
42+
| `controlled-process` | 0 | A process being controlled — the physical or data transformation acted upon by controllers. |
43+
| `controller` | 0 | A system component (human or automated) responsible for issuing control actions. Each controller has a process model — its internal beliefs about the state of the controlled process. |
44+
| `controller-constraint` | 0 | A constraint on a controller's behavior derived by inverting a UCA. Specifies what the controller must or must not do. |
45+
| `hazard` | 0 | A system state or set of conditions that, together with worst-case environmental conditions, will lead to a loss. |
46+
| `loss` | 0 | An undesired or unplanned event involving something of value to stakeholders. Losses define what the analysis aims to prevent. |
47+
| `loss-scenario` | 0 | A causal pathway describing how a UCA could occur or how the control action could be improperly executed, leading to a hazard. |
48+
| `stakeholder-req` | 0 | Stakeholder requirement (SYS.1) |
49+
| `sub-hazard` | 0 | A refinement of a hazard into a more specific unsafe condition. |
50+
| `sw-arch-component` | 0 | Software architectural element (SWE.2) |
51+
| `sw-detail-design` | 0 | Software detailed design or unit specification (SWE.3) |
52+
| `sw-integration-verification` | 0 | Software component and integration verification measure (SWE.5 — Software Component Verification and Integration Verification) |
53+
| `sw-req` | 0 | Software requirement (SWE.1) |
54+
| `sw-verification` | 0 | Software verification measure against SW requirements (SWE.6 — Software Verification) |
55+
| `sys-integration-verification` | 0 | System integration and integration verification measure (SYS.4 — System Integration and Integration Verification) |
56+
| `sys-verification` | 0 | System verification measure against system requirements (SYS.5 — System Verification) |
57+
| `system-arch-component` | 0 | System architectural element (SYS.3) |
58+
| `system-constraint` | 0 | A condition or behavior that must be satisfied to prevent a hazard. Each constraint is the inversion of a hazard. |
59+
| `system-req` | 0 | System requirement derived from stakeholder needs (SYS.2) |
60+
| `uca` | 0 | An Unsafe Control Action — a control action that, in a particular context and worst-case environment, leads to a hazard. Four types (provably complete): 1. Not providing the control action leads to a hazard 2. Providing the control action leads to a hazard 3. Providing too early, too late, or in the wrong order 4. Control action stopped too soon or applied too long |
61+
| `unit-verification` | 0 | Unit verification measure (SWE.4 — Software Unit Verification) |
62+
| `verification-execution` | 0 | A verification execution run against a specific version |
63+
| `verification-verdict` | 0 | Pass/fail verdict for a single verification measure in an execution run |
64+
65+
## Working with Artifacts
66+
67+
### File Structure
68+
- Artifacts are stored as YAML files in: `artifacts`, `safety/stpa`, `safety/stpa/requirements.yaml`, `safety/stpa/architecture.yaml`, `safety/stpa/validation.yaml`
69+
- Schema definitions: `schemas/` directory
70+
- Documents: `docs`
71+
72+
### Creating Artifacts
73+
```bash
74+
rivet add -t requirement --title "New requirement" --status draft --link "satisfies:SC-1"
75+
```
76+
77+
### Validating Changes
78+
Always run `rivet validate` after modifying artifact YAML files.
79+
Use `rivet validate --format json` for machine-readable output.
80+
81+
### Link Types
82+
83+
| Link Type | Description | Inverse |
84+
|-----------|-------------|--------|
85+
| `acts-on` | Control action acts on a process or controller | `acted-on-by` |
86+
| `allocated-to` | Source is allocated to the target (e.g. requirement to architecture component) | `allocated-from` |
87+
| `caused-by-uca` | Loss scenario is caused by an unsafe control action | `causes-scenario` |
88+
| `constrained-by` | Source is constrained by the target | `constrains` |
89+
| `constrains-controller` | Constraint applies to a specific controller | `controller-constrained-by` |
90+
| `depends-on` | Source depends on target being completed first | `depended-on-by` |
91+
| `derives-from` | Source is derived from the target | `derived-into` |
92+
| `implements` | Source implements the target | `implemented-by` |
93+
| `inverts-uca` | Controller constraint inverts (is derived from) an UCA | `inverted-by` |
94+
| `issued-by` | Control action or UCA is issued by a controller | `issues` |
95+
| `leads-to-hazard` | UCA or loss scenario leads to a hazard | `hazard-caused-by` |
96+
| `leads-to-loss` | Hazard leads to a specific loss | `loss-caused-by` |
97+
| `mitigates` | Source mitigates or prevents the target | `mitigated-by` |
98+
| `modeled-by` | An architecture component is modeled by an AADL component | `models` |
99+
| `part-of-execution` | Verification verdict belongs to a verification execution run | `contains-verdict` |
100+
| `prevents` | Constraint prevents a hazard | `prevented-by` |
101+
| `refines` | Source is a refinement or decomposition of the target | `refined-by` |
102+
| `result-of` | Verification verdict is the result of executing a verification measure | `has-result` |
103+
| `satisfies` | Source satisfies or fulfils the target | `satisfied-by` |
104+
| `traces-to` | General traceability link between any two artifacts | `traced-from` |
105+
| `verifies` | Source verifies or validates the target | `verified-by` |
106+
107+
## Conventions
108+
109+
- Artifact IDs follow the pattern: PREFIX-NNN (e.g., REQ-001, FEAT-042)
110+
- Use `rivet add` to create artifacts (auto-generates next ID)
111+
- Always include traceability links when creating artifacts
112+
- Run `rivet validate` before committing

‎CLAUDE.md‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
# CLAUDE.md
2+
3+
See [AGENTS.md](AGENTS.md) for project instructions.
4+
5+
Additional Claude Code settings:
6+
- Use `rivet validate` to verify changes to artifact YAML files
7+
- Use `rivet list --format json` for machine-readable artifact queries

‎artifacts/architecture.yaml‎

Lines changed: 128 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -477,3 +477,131 @@ artifacts:
477477
target: REQ-QUERY-001
478478
- type: traces-to
479479
target: REQ-MCP-001
480+
481+
# ── Deployment Solver Architecture ─────────────────────────────────────
482+
483+
- id: ARCH-SOLVER-001
484+
type: design-decision
485+
status: planned
486+
title: "NDS-layered hierarchical solving"
487+
description: >
488+
Deployment optimization uses 4 hierarchical layers analogous to NDS
489+
navigation. Layer 0 (Component): RTA/scheduling per processor — already
490+
implemented. Layer 1 (Cluster): bin-packing with schedulability
491+
validation — FFD/BFD heuristics in pure Rust. Layer 2 (System): topology
492+
graph extraction + bus binding optimization — petgraph-based. Layer 3
493+
(Global): cross-zone E2E + safety decomposition — exact solver
494+
(MILP/CP-SAT). Local solutions compose into globally valid configurations.
495+
fields:
496+
rationale: >
497+
Hierarchical decomposition makes NP-hard problem tractable. Each layer
498+
is independently testable. Layers 0-2 use pure Rust (WASM-compatible).
499+
Layer 3 optionally uses native solver backends.
500+
tags: [architecture, solver, v040]
501+
links:
502+
- type: satisfies
503+
target: REQ-SOLVER-004
504+
505+
- id: ARCH-SOLVER-002
506+
type: design-decision
507+
status: planned
508+
title: Topology graph as petgraph
509+
description: >
510+
Hardware topology extracted from AADL instance model into a petgraph
511+
DiGraph. Processor nodes with capacity properties (CPU budget, memory,
512+
scheduling policy). Bus edges with bandwidth and protocol properties.
513+
Memory nodes with size properties. Used as the target graph for
514+
deployment allocation.
515+
fields:
516+
rationale: >
517+
petgraph already used in spar-render for layout. Reusing it for
518+
topology avoids new dependencies. Graph operations (shortest path,
519+
connectivity, coloring) are well-supported.
520+
tags: [architecture, solver, v030]
521+
links:
522+
- type: satisfies
523+
target: REQ-SOLVER-001
524+
525+
- id: ARCH-SOLVER-003
526+
type: design-decision
527+
status: planned
528+
title: Virtual bus library as AADL package
529+
description: >
530+
Communication protocols modeled as AADL virtual bus types in a standard
531+
library package. Each virtual bus type has properties: latency_overhead,
532+
bandwidth_capacity, max_payload, security_profile, bus_type_compatibility.
533+
Solver selects from compatible virtual buses when binding connections to
534+
physical buses.
535+
fields:
536+
rationale: >
537+
Using native AADL virtual bus types means the protocol catalog is part
538+
of the model, not external configuration. Engineers can extend the
539+
library with custom protocols. spar's existing property system reads
540+
the values.
541+
tags: [architecture, solver, v030]
542+
links:
543+
- type: satisfies
544+
target: REQ-SOLVER-002
545+
546+
- id: ARCH-SOLVER-004
547+
type: design-decision
548+
status: planned
549+
title: Pure Rust bin-packing for Layer 1
550+
description: >
551+
Process-to-processor allocation uses First-Fit Decreasing (FFD) and
552+
Best-Fit Decreasing (BFD) bin-packing heuristics with schedulability
553+
validation. After tentative allocation, RTA is run per processor. If
554+
schedulability fails, the process is tried on the next candidate. Pure
555+
Rust, no external dependencies, WASM-compatible.
556+
fields:
557+
rationale: >
558+
FFD gives 11/9-approximation to optimal. Combined with RTA validation,
559+
this catches infeasible allocations immediately. Pure Rust ensures WASM
560+
compatibility. Good enough for 80% of practical use cases; exact solver
561+
handles the rest.
562+
tags: [architecture, solver, v040]
563+
links:
564+
- type: satisfies
565+
target: REQ-SOLVER-004
566+
567+
- id: ARCH-SOLVER-005
568+
type: design-decision
569+
status: planned
570+
title: Source rewriting via rowan CST
571+
description: >
572+
Solver output applied by constructing TextEdit operations on the AADL
573+
source via rowan CST. Insert/update Actual_Processor_Binding,
574+
Actual_Memory_Binding, Actual_Connection_Binding properties. Preserves
575+
formatting, comments, and all other source content. Changes validated
576+
incrementally via salsa before committing.
577+
fields:
578+
rationale: >
579+
Rowan's lossless CST preserves every byte of source. LSP code actions
580+
already use this pattern (4 existing quick-fixes). Salsa ensures only
581+
affected analyses re-run after changes.
582+
tags: [architecture, solver, v030]
583+
links:
584+
- type: satisfies
585+
target: REQ-SOLVER-007
586+
587+
- id: ARCH-SOLVER-006
588+
type: design-decision
589+
status: planned
590+
title: "Dual solver strategy (WASM heuristic + native exact)"
591+
description: >
592+
Two solver tiers. Tier 1 (WASM): pure Rust heuristics (FFD/BFD
593+
bin-packing, NSGA-II for Pareto). Runs in browser and CLI. Tier 2
594+
(native): exact solver via good_lp+HiGHS (MILP) or cp_sat (CP-SAT).
595+
Returns optimality certificates. CLI only due to C++ dependencies.
596+
fields:
597+
rationale: >
598+
WASM compatibility for Tier 1 enables browser-based architecture
599+
exploration. Tier 2 provides formal guarantees for certification
600+
evidence. Engineers start with Tier 1 for interactive exploration,
601+
then run Tier 2 for final optimization.
602+
tags: [architecture, solver, v040]
603+
links:
604+
- type: satisfies
605+
target: REQ-SOLVER-005
606+
- type: satisfies
607+
target: REQ-SOLVER-006

‎artifacts/requirements.yaml‎

Lines changed: 107 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -585,3 +585,110 @@ artifacts:
585585
and aggregation.
586586
status: planned
587587
tags: [query, instance, v030]
588+
589+
# ── Deployment Solver (v0.4.0+) ──────────────────────────────────────
590+
591+
- id: REQ-SOLVER-001
592+
type: requirement
593+
title: Hardware topology graph extraction
594+
description: >
595+
Extract a petgraph from the AADL instance model representing the
596+
hardware topology: processors as nodes, buses as edges, with capacity
597+
properties (CPU budget, memory size, bus bandwidth). Serves as the
598+
target graph for deployment optimization.
599+
status: planned
600+
tags: [solver, topology, v030]
601+
602+
- id: REQ-SOLVER-002
603+
type: requirement
604+
title: Virtual bus library (communication protocol catalog)
605+
description: >
606+
AADL package library defining virtual bus types for common protocols:
607+
DDS, SOME/IP, shared memory, CAN, CAN FD, Ethernet, AFDX, SpaceWire,
608+
PROFINET, EtherCAT, MAVLink. Each includes latency overhead, bandwidth,
609+
max payload, security profile, and bus type compatibility properties.
610+
status: planned
611+
tags: [solver, protocol, v030]
612+
613+
- id: REQ-SOLVER-003
614+
type: requirement
615+
title: Constraint formulation from AADL properties
616+
description: >
617+
Translate AADL model properties into solver constraints: timing
618+
(Period, Deadline, WCET → scheduling feasibility), safety (ASIL/DAL
619+
→ partition isolation), security (trust zones → encryption overhead),
620+
resources (memory/CPU/bandwidth budgets), physical (bus connectivity).
621+
status: planned
622+
tags: [solver, constraints, v030]
623+
624+
- id: REQ-SOLVER-004
625+
type: requirement
626+
title: Hierarchical deployment solving (NDS-layered)
627+
description: >
628+
Solve deployment in hierarchical layers analogous to NDS navigation:
629+
Layer 0 (Component) — schedule threads within one processor (RTA).
630+
Layer 1 (Cluster) — allocate processes to processors within a
631+
subsystem (bin packing + schedulability). Layer 2 (System) — allocate
632+
subsystems to hardware zones (topology + bandwidth + safety). Layer 3
633+
(Global) — optimize across all zones (E2E latency, safety decomposition,
634+
cost). Local solutions compose into globally valid configurations.
635+
status: planned
636+
tags: [solver, optimization, v040]
637+
638+
- id: REQ-SOLVER-005
639+
type: requirement
640+
title: Optimality certificates for deployment solutions
641+
description: >
642+
Deployment solver returns not just a valid configuration but a
643+
machine-checkable certificate proving it is globally optimal (for
644+
exact methods) or within a bounded optimality gap (for heuristics).
645+
Uses dual bounds from MILP or exhaustive search proofs from CP-SAT.
646+
status: planned
647+
tags: [solver, verification, v040]
648+
649+
- id: REQ-SOLVER-006
650+
type: requirement
651+
title: Multi-objective Pareto front computation
652+
description: >
653+
For conflicting objectives (minimize latency vs minimize cost vs
654+
maximize safety margins), compute the Pareto front of non-dominated
655+
solutions. Present to the engineer for interactive selection. Support
656+
both exact Pareto (small problems) and approximate (NSGA-II for large).
657+
status: planned
658+
tags: [solver, optimization, v040]
659+
660+
- id: REQ-SOLVER-007
661+
type: requirement
662+
title: Source rewriting to apply deployment solutions
663+
description: >
664+
Apply solver output by rewriting AADL source via rowan CST
665+
manipulation. Insert/update Actual_Processor_Binding, Actual_Memory_Binding,
666+
Actual_Connection_Binding properties. Preserve formatting and comments.
667+
Validate incrementally via salsa after each change.
668+
status: planned
669+
tags: [solver, refactoring, v030]
670+
671+
- id: REQ-SOLVER-008
672+
type: requirement
673+
title: Safety decomposition validation (ASIL/DAL/SIL)
674+
description: >
675+
Validate that ASIL decomposition rules are satisfied in the deployment:
676+
decomposed requirements are allocated to sufficiently independent elements,
677+
freedom from interference is ensured (spatial via MMU, temporal via
678+
scheduling, communication via controlled interfaces). Supports ISO 26262
679+
ASIL, DO-178C DAL, and IEC 61508 SIL.
680+
status: planned
681+
tags: [solver, safety, v040]
682+
683+
- id: REQ-SOLVER-009
684+
type: requirement
685+
title: Security zone and conduit validation
686+
description: >
687+
Model IEC 62443 / ISO 21434 security zones as AADL system components
688+
with security-level properties. Validate that cross-zone connections
689+
have appropriate protection (encryption, authentication). Account for
690+
security overhead (TLS latency, MAC computation) in timing analysis.
691+
status: planned
692+
tags: [solver, security, v040]
693+
694+
# Research findings tracked separately in research/findings.yaml

0 commit comments

Comments
 (0)