Skip to content

docs(readme): reframe as a compiler for system-architecture models #286

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
avrabe merged 1 commit into from
Jun 14, 2026
Merged

docs(readme): reframe as a compiler for system-architecture models #286

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
163 changes: 134 additions & 29 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,13 +2,15 @@

# Spar

<sup>AADL v2.3 toolchain + deployment solver</sup>
<sup>a compiler for system-architecture models</sup>

&nbsp;

![Rust](https://img.shields.io/badge/Rust-CE422B?style=flat-square&logo=rust&logoColor=white&labelColor=1a1b27)
![WebAssembly](https://img.shields.io/badge/WebAssembly-654FF0?style=flat-square&logo=webassembly&logoColor=white&labelColor=1a1b27)
![AADL](https://img.shields.io/badge/AADL_v2.3-AS5506D-654FF0?style=flat-square&labelColor=1a1b27)
![SysML](https://img.shields.io/badge/SysML_v2-KerML-654FF0?style=flat-square&labelColor=1a1b27)
![TSN](https://img.shields.io/badge/TSN-Network_Calculus-654FF0?style=flat-square&labelColor=1a1b27)
![License: MIT](https://img.shields.io/badge/License-MIT-blue?style=flat-square&labelColor=1a1b27)

[![CI](https://github.com/pulseengine/spar/actions/workflows/ci.yml/badge.svg)](https://github.com/pulseengine/spar/actions/workflows/ci.yml)
Expand Down Expand Up @@ -36,9 +38,88 @@

&nbsp;

A Rust implementation of a complete AADL (Architecture Analysis and Design Language) toolchain. Parses, validates, analyzes, transforms, and visualizes system architectures per SAE AS5506D. Includes a deployment solver for automated thread-to-processor allocation. Designed for safety-critical systems modeling -- avionics, vehicle software, WASM component architectures, and AI agent workflows.

Spar replaces the Eclipse/Java-based OSATE2 toolchain with a fast, embeddable, WASM-compilable alternative built on rust-analyzer's proven architecture patterns.
Spar is a **compiler for system-architecture models**, built on rust-analyzer's proven
architecture patterns. Like a programming-language compiler it has *front-ends* (parsers for
several modelling formalisms), a shared *intermediate representation* (an incremental,
salsa-backed HIR), a *middle-end* of analyses, and *back-ends* that emit code and diagrams —
except the "programs" it compiles are **system architectures**.

- **Front-ends — multi-formalism ingest.** AADL v2.3 (SAE AS5506D), SysML v2 / KerML, and
CAN `.dbc` networks all lower into one semantic model. ARXML (AUTOSAR) is on the roadmap.
- **Middle-end — analysis & timing.** 30+ pluggable passes (scheduling, EMV2 fault trees,
ARINC 653 partitioning, ASIL decomposition, resource budgets) plus a real-time
**network-calculus** engine (TFA / PLP) that computes worst-case TSN/Ethernet latency bounds —
the kind of timing analysis usually reserved for tools like tsnkit, RTaW-Pegase or pegase.
- **Back-ends — generate & visualize.** WIT/WASM components, Lean 4 and Kani proof skeletons,
Bazel build files, SVG and Mermaid architecture diagrams.
- **Verified by construction.** Every capability is traced to a requirement (rivet artifacts),
oracle-gated in CI, and exposed read-only to AI agents over MCP.

This is why it has outgrown the "AADL toolchain" label: AADL is one of several front-ends, and
the timing/verification middle-end is a substrate any architecture formalism can feed. Spar
replaces the Eclipse/Java OSATE2 toolchain with a fast, embeddable, WASM-compilable alternative —
and reaches well past what OSATE, or a single-formalism SysML v2 tool, covers.

## Components

```mermaid
flowchart TB
subgraph FE["Front-ends · multi-formalism ingest"]
AADL["spar-parser · spar-syntax · spar-annex<br/>AADL v2.3 — lossless CST + annexes (EMV2, BA)"]
SYSML["spar-sysml2<br/>SysML v2 / KerML → AADL lowering"]
DBC["spar-dbc<br/>CAN .dbc → AADL"]
end

subgraph IR["Semantic core · incremental IR"]
DB["spar-base-db<br/>salsa incremental DB"]
HIRDEF["spar-hir-def<br/>item tree · instance model"]
HIR["spar-hir<br/>semantic facade"]
VAR["spar-variants<br/>product-line / variant filtering"]
end

subgraph MID["Middle-end · analysis & timing"]
ANL["spar-analysis<br/>30+ passes: scheduling, EMV2 fault trees,<br/>ARINC 653, ASIL, budgets"]
NET["spar-network<br/>Network Calculus TFA / PLP<br/>TSN / Ethernet WCTT bounds"]
SOL["spar-solver<br/>thread→processor deployment"]
TOPO["spar-trace-topology<br/>PCAPNG+LLDP vs declared topology"]
INS["spar-insight<br/>CTF trace vs predicted timing"]
end

subgraph BE["Back-ends · generate & visualize"]
GEN["spar-codegen<br/>WIT · Rust · Lean 4 · Kani · Bazel"]
TR["spar-transform<br/>AADL ↔ WIT / WAC / wRPC"]
REN["spar-render<br/>SVG (Sugiyama layout)"]
MMD["spar-mermaid<br/>Mermaid diagrams"]
end

subgraph IF["Interfaces"]
CLI["spar-cli<br/>16 subcommands incl. LSP + MCP"]
MCP["spar-mcp<br/>read-only oracles for AI agents"]
WASM["spar-wasm<br/>WASI P2 / browser component"]
end

VFY["spar-verify · spar-verify-macros<br/>requirements assertion engine"]

AADL --> DB
SYSML --> DB
DBC --> DB
DB --> HIRDEF --> HIR --> VAR
HIR --> ANL
HIR --> NET
HIR --> SOL
HIR --> TOPO
HIR --> INS
ANL --> VFY
NET --> VFY
HIR --> GEN
HIR --> TR
HIR --> REN
HIR --> MMD
CLI --> HIR
MCP --> HIR
WASM --> HIR
GEN -->|WIT components| DOWN["PulseEngine chain →<br/>witness · sigil · smithy · loom"]
```

## Installation

Expand Down Expand Up @@ -85,46 +166,70 @@ spar verify --root Pkg::System.Impl --rules rules.toml vehicle.aadl
| `analyze` | Run all analysis passes (SARIF/JSON/text output) |
| `allocate` | Solve thread-to-processor deployment bindings |
| `diff` | Compare two model versions for structural/diagnostic changes |
| `modes` | List operational modes and mode transitions |
| `modes` | Mode reachability analysis and SMV/DOT export |
| `emit` | Emit a Mermaid flowchart from an instantiated system |
| `render` | Generate SVG/HTML architecture diagrams |
| `verify` | Evaluate verification assertions against the model |
| `codegen` | Generate code (WIT/Rust/Lean4/Kani/Bazel) from an instance |
| `dbc` | Ingest a CAN `.dbc` file and emit AADL (bus + devices) |
| `moves` | Hypothetical-rebinding oracle (verify a move under overlay) |
| `insight` | Compare CTF timing traces to Expected_BCET/WCET/Mean |
| `lsp` | Start the Language Server Protocol server |
| `mcp` | Start the MCP server (read-only oracles for AI agents) |

## Architecture

20 crates, layered from low-level parsing to high-level analysis:
23 crates, organized as compiler stages — front-ends → IR → middle-end → back-ends:

```
spar-syntax Lossless CST (rowan red-green trees)
spar-parser Recursive descent parser with error recovery
spar-annex AADL annex sublanguage parsing (EMV2, BLESS, BA)
spar-base-db Salsa database for incremental computation
spar-hir-def HIR definitions -- item tree, instance model, arenas
spar-hir Public semantic facade (name resolution, properties)
spar-analysis 30 pluggable analysis passes
spar-transform Format transforms (AADL <-> WIT, WAC, Rust crates, wRPC)
spar-solver Deployment solver (thread-to-processor allocation)
spar-render SVG architecture diagrams (compound Sugiyama layout)
spar-network Network topology and WCTT analysis support
spar-variants Product-line variant selection and HIR filtering
spar-verify Requirements verification engine
spar-verify-macros Procedural macros for verification rules
spar-codegen Rust + WIT code generation from instance models
spar-insight Discrepancy assistant (compare CTF traces vs expected)
spar-sysml2 SysML v2 / KerML extraction and generation
spar-mcp Model Context Protocol server (read-only oracles)
spar-cli Command-line interface
spar-wasm WebAssembly component (WASI P2)
Front-ends (ingest)
spar-syntax Lossless CST (rowan red-green trees) + typed AST
spar-parser AADL recursive-descent parser with error recovery
spar-annex AADL annex sublanguages (EMV2, BA, BLESS)
spar-sysml2 SysML v2 / KerML parser + AADL lowering + requirements
spar-dbc CAN .dbc ingest -> AADL source text

Semantic core (intermediate representation)
spar-base-db Salsa database for incremental computation
spar-hir-def HIR definitions -- item tree, instance model, arenas
spar-hir Public semantic facade (name resolution, properties)
spar-variants Product-line variant selection and HIR filtering

Middle-end (analysis & timing)
spar-analysis 30+ pluggable analysis passes
spar-network Network Calculus (TFA/PLP) -- TSN/Ethernet WCTT bounds
spar-solver Deployment solver (thread-to-processor allocation)
spar-trace-topology Runtime vs declared topology (PCAPNG + LLDP + Qcc)
spar-insight Discrepancy assistant (CTF traces vs predicted timing)

Verification
spar-verify Requirements verification / assertion engine
spar-verify-macros Procedural macros for verification rules

Back-ends (generate & visualize)
spar-codegen Codegen from instance models (WIT, Rust, Lean4, Kani, Bazel)
spar-transform Format transforms (AADL <-> WIT, WAC, wRPC)
spar-render SVG architecture diagrams (compound Sugiyama layout)
spar-mermaid Mermaid diagram emission

Interfaces
spar-cli Command-line interface (16 subcommands incl. LSP + MCP)
spar-mcp Model Context Protocol server (read-only oracles)
spar-wasm WebAssembly component (WASI P2 / browser)
```

## Key Features

- **30 analysis passes** -- scheduling, latency, connectivity, resource budgets, ARINC 653, EMV2 fault trees, bus bandwidth, weight/power, mode reachability, and more
- **Multi-formalism ingest** -- AADL v2.3, SysML v2 / KerML, and CAN `.dbc` all lower into one semantic model (ARXML on the roadmap)
- **30+ analysis passes** -- scheduling, latency, connectivity, resource budgets, ARINC 653, ASIL, EMV2 fault trees, bus bandwidth, weight/power, mode reachability, and more
- **Network-calculus timing** -- worst-case TSN/Ethernet latency bounds via Total-Flow (TFA) and Polynomial-LP (PLP) analysis, cross-validated against the panco reference ([Bouillard](https://arxiv.org/abs/2010.09263))
- **Assertion engine** -- declarative verification rules in TOML (`spar verify`)
- **Deployment solver** -- automated thread-to-processor allocation with constraint satisfaction
- **Code generation** -- WIT/WASM components, Lean 4 + Kani proof skeletons, Bazel build files
- **AI-agent native** -- read-only verification oracles exposed over MCP (`spar mcp`)
- **SARIF output** -- analysis results in SARIF format for CI integration
- **VS Code extension** -- live AADL rendering and diagnostics via LSP
- **WASM component** -- compiles to a 1.3 MB wasm32-wasip2 component
- **VS Code extension** -- live rendering and diagnostics via LSP
- **WASM component** -- compiles to a wasm32-wasip2 component
- **Incremental** -- salsa-based memoization for fast re-analysis
- **Lossless parsing** -- every byte preserved in the syntax tree

Expand Down
Loading