ADCS Lifecycle Demo

Site: https://dynamicalsystemsgroup.github.io/ADCS-lifecycle-demo/: every presentation, one card per artifact.

One satellite, one requirement, several presentations. This repo is a running workspace for building and presenting demos about evidence, attestation and requirements traceability. It always uses the same subject example: the attitude determination and control system (ADCS) of a geosynchronous communications satellite, and REQ-001, which says pointing error settles within 0.1° within 120 s of a slew. Each presentation adds a new artifact with a new toolchain, and the earlier ones stay runnable.

Evidence does not verify requirements; evidence supports a human judgment that requirements are satisfied.

Presentations

Date	Venue	Artifact	Toolchain	Run it	On the site
2026-05-22	OpenMBEE community call (Flexo/SysML v2 dev meeting)	notebook.py	marimo, RDF (PROV, EARL, GSN), SHACL, SymPy, SciPy	uv run marimo run notebook.py	notebook
2026-06-12	JAXA MBSE/MCE Workshop, Presentations from Industry (Tsukuba)	intro slides (PDF, site/jaxa-intro-slides.pdf) + jaxa_notebook.ipynb	Jupyter, rdflib, Flexo MMS (Layer 1), behavior-model oracle	uv run jupyter lab jaxa_notebook.ipynb	slides, notebook
2026-06-18	INCOSE International Symposium 2026 (a related paper; not the satellite example)	paper + talk slides (PDF, site/incose-is-2026-slides.pdf)	knowledgecomplex (OWL, SHACL, SPARQL)	see that repo	slides
2026-10-15	Open Source Architects (OSA) Community	talk.py, slides and live demo in one marimo app	marimo, SysML v2 (OpenSysML), Flexo MMS SysML v2 API, z3, PlantUML, Git	uv run marimo run talk.py (Run the talk)	deck, a static pre-signed export · recording

The INCOSE IS 2026 paper is a companion piece. Instead of the satellite, it assures its own documents, applying the same split to documents: machine verification against a specification, an accountable human validation against guidance, and assurance as the closed triangle between them.

Two audiences, one example. The two big talks are duals. JAXA was for systems engineers learning open-source software practice: a vendor-neutral, open-source spine (RDF standards, Python, Flexo MMS) keeps evidence and judgment traceable across tools. OSA was for open-source software architects learning systems engineering practice: requirements as behavioral envelopes, evidence with blind spots, and a person's judgment on the record, made continuous like CI/CD. They share a title because the OSA invitation came from the JAXA talk and the OpenMBEE work, so the public abstract kept the JAXA title. The tools changed too: OpenMBEE released OpenSysML in August 2026, so JAXA is the RDF edition and OSA is the SysML v2 edition (see below).

The framework

The OSA talk frames the record in four layers, DEER: Declaration, Execution, Evidence, Realization. Declaration covers architecture and requirements (SysML v2, stored in Flexo MMS). Execution covers scenarios and analysis pipelines (software, in Git). Evidence covers data from measurements, simulations and analyses (datasets, in append-only stores). Realization covers infrastructure and images (build artifacts, in an artifact registry; see Governed Compute, End to End). Open-source software is the layer that carries engineering standards into code that engineering environments import and organizations use; organizations feed back by choosing and provisioning tools, by sponsoring and maintaining the software, and through standards working groups. The site's Framework tab has both pictures.

The take-away

A tool says pass. A person says satisfied. The tool's formal result is about the model; the human attestation is about the system the model represents.

1. Requirements declare behavioral envelopes: ranges of acceptable behavior, under stated operating assumptions. Without one, "working as intended?" has no answer.
2. Every kind of evidence has a blind spot. Model checking, simulation, symbolic analysis and tests each miss something, and none of them is the spacecraft. Contradictory evidence is expected.
3. CI/CD becomes CA/CP: continuous analysis, continuous publication. Every design change re-runs the analyses and republishes the model. Automation alone is an open loop. A qualified engineer closes it, as a reviewer does for a pull request, and their judgment, with rationale, becomes part of the model.

The site is built by .github/workflows/publish.yml on every push to main. The landing page is site/index.html, and each artifact is exported fresh: marimo export html, Jupyter nbconvert of the recorded outputs, and the PDF as committed. The OSA deck needs local tools and a Flexo server for its live steps, so it cannot run in the browser. The site carries its static export, with every demo step pre-signed and nothing published to Flexo.

Adding a presentation

1. Build the new artifact at the repo root, next to the others (e.g. <venue>_notebook.py), and reuse the shared code below rather than forking it.
2. Add a row to the table above and a card to site/index.html.
3. Add an export step to publish.yml that writes _site/<venue>/.

How this repo is organized

All the presentations share one subject and two code bases:

• The RDF edition (May and June 2026) holds the traceability as RDF named graphs: ontology/, structural/, analysis/, evidence/, traceability/, pipeline/, compute/, interrogate/, documents/, flexo/. notebook.py and jaxa_notebook.ipynb drive it. Most of this README documents it, from Setup down.
• The SysML v2 edition (October 2026) writes the model, evidence and attestation in SysML v2: sysml/ (model, evidence engine, Flexo SysML v2 client) and talk/ (slide fragments and assets). talk.py drives it, and it reuses analysis/ for the simulation and the symbolic estimate.
• site/ is the landing page. private/ (gitignored) holds speaker notes and content that is not public.

Architecture: see ARCHITECTURE.md: the three-remote (git + Flexo + local Docker) + fourth-service (CouchDB txnlog) picture of the RDF edition. AI-aided engineering loop: see ENGINEERING_LOOP.md: how the LLM agent is constrained by CLIs, p-plan sequencing, and SHACL closure rules, with validation reserved for the accountable engineer.

Run the talk (the SysML v2 edition)

talk.py is one marimo notebook that is both the slide deck and the live demo: one cell is one slide, in file order (slides layout in layouts/talk.slides.json). Nineteen slides; the order is in talk/slides/order.txt.

bash scripts/fetch_tools.sh                             # once: sysml, sysmlv2, plantuml.jar into .tools/
uv run marimo run talk.py                               # present
SYSML_DEMO_PRESEED=1 uv run marimo export html talk.py -o output/talk.html   # static fallback

• Start it ahead of time and let it finish loading. Everything heavy is computed at load: the evidence for the three designs on all three slew axes, the 3x3 gain grid, the in-model solver-step runs and the z3 box (sysml.evidence.precompute, cached under output/ by a hash of the analysis code; the first cold run takes about 40 s, a warm one a few seconds).
• Static slides are HTML fragments in talk/slides/ (see talk/slides/README.md). Builds on them are CSS-only: click the small numbered circles at the bottom right. Scripts in mo.Html are stripped, so there is no keyboard build.
• Demo slides (D1, D2, D3) are precomputed and instant: the step selector (small radio buttons, bottom right), the time slider and the torque-limit and solver-step toggles only read precomputed results. Three things are live, each with a labelled fallback:
  • the z3 line, sysmlv2 verify sysml/linear_region_toolkit.sysml --solve (needs .tools/sysmlv2 and z3). Fallback: talk/assets/tool-verify.txt, labelled "captured";
  • the Attest click, which writes the person's claim into the model, evaluates it and publishes the snapshot to Flexo (tagged git-<sha>). Fallback: a row labelled "local mode";
  • the regenerated requirement view on D3 (sysml.views.requirement_view, then PlantUML; needs Java). Fallback: talk/assets/tool-req-c3.svg, labelled "captured".
• Flexo. Set FLEXO_V2_URL (default http://localhost:8083, see sysml/FLEXO_LOCAL.md). The notebook probes it once at load and uses one project per Git SHA, sysml-talk-<sha7>. A publish takes about 17 s on the local stack and shows "Publishing…" meanwhile. Without a reachable Flexo it runs in local mode and the commit row says so.
• DRAFT wording. The D2 (4, 25) card and rationale are DRAFT: the card carries a visible DRAFT tag until C2_TEXT_SIGNED_OFF in sysml/model.py is set to True, which is done only when the speaker approves the wording.
• Engineer name. The recorded attestations carry SYSML_DEMO_ENGINEER (default: the name in sysml/model.py).
• Static export. SYSML_DEMO_PRESEED=1 shows each demo slide in its final state, pre-signed, and never publishes to Flexo.
• Fault injection. FLEXO_V2_URL=http://127.0.0.1:1, OPENSYSML_SMT=/nonexistent (no z3) and SYSML_TOOLS_DIR=/nonexistent (no .tools/) each degrade to a labelled fallback, not a crash.
• The Kotar captures in talk/assets/ are screenshots only. uv run python scripts/talk_check.py --private <private dir> checks the notes against the slides; uv run python scripts/speaker_notes.py regenerates the companion notes.

The RDF edition

Bidirectional requirements traceability for the ADCS, demonstrating the full lifecycle from SysMLv2 structural specification through symbolic analysis, numerical simulation, and human expert attestation. The RTM is held as an rdflib.Dataset of named graphs, verified by a SHACL closure-rule suite, audited forward and backward independently, and exportable to disk, to a Flexo MMS instance, or to bare Apache Jena Fuseki.

Setup

# Install deps
uv sync

# Copy + edit env vars (Flexo token, txnlog opt-in, org auspices)
cp .env.example .env
$EDITOR .env

The canonical multi-remote run additionally needs the local txnlog store (a CouchDB container) running:

tools/start-services.sh    # docker run + db ensure, idempotent
# ...later
tools/stop-services.sh     # stop + remove (--purge wipes the volume)

Preflight at the start of every pipeline run probes every configured backend (Flexo, Docker daemon, txnlog) and fails fast (exit 2) if anything is unreachable. The integration story does not silently degrade.

Core Principle

Evidence does not verify requirements; evidence supports a human judgment that requirements are satisfied.

Models are imperfect representations of physical systems. Symbolic proofs and simulation results are claims true within the model. The engineer judges model adequacy and evidence sufficiency. Only human attestation connects evidence to requirement satisfaction.

This split is not novel — it is the canonical Hawkins–Habli Assurance Claim Point categorization. In this demo, adequacy is a gsn:Assumption and sufficiency is a gsn:Justification, both linked to the attestation via gsn:inContextOf. rtm: adds no novel epistemic vocabulary; it is a thin integration layer over established standards.

Architecture

Integration ontology assembled from W3C and OMG standards plus the OMG SysMLv2 OWL rendering:

Layer	Vocabulary	Role
W3C / IETF	prov:, dcterms:, earl:, sh:	Provenance + assertion + outcome + SHACL closure
OMG / SysML	sysml: ↔ omg-sysml:	Structural model + requirements (aliased to the OMG SysMLv2 OWL rendering via owl:equivalentClass)
Community	gsn:, p-plan:	Assurance argument structure + declarative process model
Tool interop	oslc_rm:, oslc_qm:	Aliases for DOORS Next / Jama / RQM
Local glue	rtm:	Convenience subclasses + content-addressing properties only

See ontology/rtm-edit.ttl for the source and ontology/assembly_manifest.json for the build-time manifest.

Named-Graph Quadstore Layout

The runtime holds the RTM as an rdflib.Dataset with one named graph per content layer — sized to match how Flexo MMS partitions projects/branches:

Named graph	Contents
<rtm:ontology>	TBox + shapes + individuals (from ontology/*.ttl)
<rtm:plan>	P-PLAN process model (pipeline/plan.ttl)
<adcs:structural>	SysMLv2 instance data (satellite + parameters)
<adcs:context>	Stable gsn:Context / gsn:Assumption individuals
<adcs:evidence>	Generated rtm:ProofArtifact / rtm:SimulationResult
<adcs:attestations>	rtm:Attestation events + adequacy / sufficiency nodes
<adcs:plan-execution>	p-plan:Activity instances (one per stage)
<adcs:audit>	Audit report summary triples (forward/backward results)

SPARQL queries use Dataset(default_union=True) so existing queries match across the union without GRAPH clauses.

Quick Start

uv sync
uv run python -m pipeline.runner --auto       # local + local (fastest path)
uv run python -m pipeline.runner               # interactive attestation
uv run pytest -v                                # default: skips live + network markers

Canonical multi-remote run (the architecture's full picture)

After completing Setup above and exporting ADCS_TXNLOG_ENABLED=1 (plus FLEXO_TOKEN), the canonical run exercises all three remotes

• the txnlog store:

tools/start-services.sh
export ADCS_TXNLOG_ENABLED=1
uv run python -m pipeline.runner --auto --backend=flexo --compute=docker

The runner's preflight verifies every backend before Stage 0; if any remote is unreachable, the run fails fast (exit 2) with a concrete cause. The output rtm.trig carries the full provenance chain documented in ARCHITECTURE.md.

Reproducibility verification

compute.reproduce rebuilds an image at its recorded git ref and digest-compares:

uv run python -m compute.reproduce \
    --image-digest sha256:71a59f23... \
    --from-trig output/rtm.trig

Exit 0 = digest matches; 1 = mismatch; 2 = prerequisite failure. Outcome is also recorded as an rtm:DigestMatchAssertion in <adcs:audit>.

Behavior-model oracle

analysis.oracle compares a behavior-model output metric (e.g. simulated settling_time_s) against a requirement's machine-readable acceptance criterion and records the outcome as an rtm:BehaviorOracleAssertion (earl:mode = earl:automatic) in <adcs:audit>, beside the closure-rule and digest-match assertions. This is verification of a model-level claim ("the metric meets/exceeds the budget, within the model") — it never asserts that the physical requirement is satisfied. Only human attestation does that, so the oracle links the requirement via rtm:evaluatesAgainst, never rtm:attests. When a requirement has no machine-readable criterion (REQ-004), the oracle returns earl:cantTell rather than fabricating a verdict.

Tests

uv run pytest               # default: skips live + network markers
uv run pytest -m live       # opt-in: round-trips against a live Flexo MMS (needs FLEXO_TOKEN)
uv run pytest -m network    # opt-in: reserved for W3C-vocab fetches (no tests today)

Marker filtering is set in pyproject.toml via addopts = "-m 'not live and not network'" so the canonical invocation never hits external services. CI opts in explicitly per workflow.

Pipeline Stages

[Stage 0]   Ontology Assembly         — narrate the integration; load TBox into <rtm:ontology>
[Stage 1]   Structural Model          — load SysMLv2 instance data into <adcs:structural>
[Stage 2]   Symbolic Analysis         — SymPy: inertia, eigenvalues, stability proofs
[Stage 3]   Numerical Simulation      — scipy: step response + disturbance rejection
[Stage 4]   Evidence Binding          — emit hashed evidence into <adcs:evidence>
[Stage 5]   RTM Assembled             — verify evidence completeness
[Stage 6]   Human Attestation         — emit attestations into <adcs:attestations>
[Stage 6.5] Verify Closure-Rule Suite — 9 SHACL shapes + runtime re-verification
[Stage 7a]  Audit Trace               — forward / backward / bidirectional + coverage matrix
[Stage 7]   Generate Reports          — persist via backend, write output/audit.{md,csv}
[Stage 8]   Interrogate               — explain / reproduce / visualize ready

Stage 0 banner (first thing you see)

[Stage 0/8] Ontology Assembly
─────────────────────────────────────────────────────────────────
  Loading assembled rtm.ttl (built 2026-05-14T01:26:27Z from rtm-edit.ttl)
  Imports resolved:
    OK  EARL         162 triples,  5 terms referenced
    OK  OSLC QM       90 triples,  1 terms referenced
    OK  OSLC RM       74 triples,  1 terms referenced
    OK  OntoGSN     3784 triples,  3 terms referenced
    OK  P-PLAN       154 triples,  0 terms referenced
    OK  PROV-O      1146 triples,  7 terms referenced
  SysMLv2 equivalence axioms: 9
  Local rtm: integration glue: 13 subclass + 7 subproperty axioms
  Verification: ROBOT merge + ELK reasoning + OBO report PASS
  Loaded into <rtm:ontology>: 317 triples
  Closure-rule suite registered: 13 SHACL shapes
─────────────────────────────────────────────────────────────────

Pipeline architecture

The orchestrator threads a PipelineState object through per-stage free functions (run_stage_<N>_<name>(state) -> <StageResult> in pipeline/runner.py). Each stage returns a frozen dataclass that the next stage reads via state.<prior>.<field>, so the runner is the call sequence plus narration — the per-stage logic stands alone and is unit-testable. The activity_to_stage table on PipelineState maps p-plan step IRI fragments to stage numbers; interrogate.rerun consumes the same mapping to translate closure-rule violations into the stages that must re-run.

All CLIs are Typer apps; --help is auto-rendered with rich formatting. Tests use typer.testing.CliRunner (tests/test_cli.py).

Interrogation

from pipeline.runner import run_pipeline
from interrogate.explain import explain_requirement

rtm = run_pipeline(auto_attest=True)
print(explain_requirement(rtm, "REQ-003"))

Produces a dereferenceable explanation chain:

REQ-003: "The closed-loop ADCS shall be asymptotically stable..."
├── Derived from: SAT-REQ-STABILITY
├── Allocated to: PDController
├── Evidence (1 artifacts):
│   └── [ProofArtifact]
│       Re-verification: VERIFIED (re-executed just now)
│         characteristic_polynomial_form: ✓
│         routh_row0_positive: ✓
│         routh_row1_positive: ✓
│         routh_row2_positive: ✓
└── Attestation:
    Outcome: earl:passed (mode: earl:semiAuto)
    Attested by: Dr. Michael Zargham (@mzargham)
    Model adequacy: "Linearized stability analysis via Routh-Hurwitz..."
    Evidence sufficiency: "Routh-Hurwitz proof confirms asymptotic..."

Rerun plan from a verification report

When the Stage 6.5 SHACL suite or the runtime re-verification finds a mismatch, interrogate/rerun.py walks prov:wasGeneratedBy -> p-plan:correspondsToStep to translate the violations into the dedup'd ordered set of pipeline stages that must re-run. SHACL violations on structural / human-judgement nodes (attestations, etc.) are reported separately — no stage re-run can fix them.

uv run python -m interrogate.rerun                    # markdown to stdout
uv run python -m interrogate.rerun --requirement REQ-003
uv run python -m interrogate.rerun --format json

Exit code 0 = clean, 1 = stages or structural violations present, 2 = input file not found. The Stage 6.5 banner in the runner also prints a short rerun-plan summary when violations are present.

Compiled design document (a view over the RDF)

documents/design_description.py compiles DDVS-001 — ADCS Design Description & Verification Status, a classic engineering document rendered deterministically from the persisted dataset: derivation and allocation tables, a Verification Cross-Reference Matrix, per-requirement evidence + attestation detail with the GSN adequacy/sufficiency statements, and a colophon with per-graph triple counts and the dataset's SHA-256 fingerprint. The compiler never consults the wall clock (the document date is the max prov:generatedAtTime in the data), so identical input bytes rebuild to byte-identical Markdown.

uv run python -m documents.design_description          # → output/design_description.md
uv run python -m documents.design_description --stdout --requirement REQ-003
uv run python -m documents.design_description --check   # drift gate: exit 1 if stale

The built document carries an AUTO-GENERATED header — rebuild it, don't edit it (same discipline as ontology/rtm.ttl). Exit codes: 0 = built / up to date, 1 = --check drift, 2 = input or checked output missing.

Requirements

ID	Requirement	Outcome (default run)
REQ-001	Pointing accuracy < 0.1 deg within 120s	earl:failed (declined — settling time exceeds spec)
REQ-002	Wheel momentum < 4.0 N.m.s	earl:passed
REQ-003	Closed-loop stability: Re(λ) ≤ -0.010	earl:passed
REQ-004	Gravity gradient rejection at GEO	earl:passed

REQ-001 is intentionally a declined attestation (a well-formed rtm:Attestation with earl:failed outcome) so the closure-rule suite has a realistic case where the audit must distinguish "no attestation" from "attested-but-not-passing."

Closure-Rule Suite

Ten machine-checkable invariants. Nine are SHACL shapes in ontology/rtm_shapes.ttl; the tenth is a runtime re-verification check (interrogate/reproduce).

1. AttestationShape — adequacy Assumption + sufficiency Justification + outcome + qualified association
2. PlanInstantiationShape — every p-plan:Activity corresponds to a known step
3. EvidenceShape — hashes + source + generating activity + addresses a requirement
4. RequirementShape — declared name + text
5. GsnArgumentShape — Goal → Strategy → Solution chain; non-empty statements
6. ProvenanceShape — Activity has Agent; Entity has ≤1 generating activity
7. OutcomeSemanticsShape — outcome-specific rationale requirements
8. ForwardTraceabilityShape / BackwardTraceabilityShape — independent; bidirectional is the conjunction
9. NamedGraphIntegrityShape — cross-graph references resolve
10. Re-verification closure (runtime) — every rtm:ProofArtifact re-hashes to its stored rtm:proofHash

Run at pipeline time as Stage 6.5; report lands in <adcs:audit>.

Audit (Stage 7a)

Forward and backward traceability checks run independently and emit separate failure lists, so error messages identify which direction broke:

[Stage 7a] Auditing forward / backward / bidirectional traceability...
  Forward    PASS  (4 checked, 0 failures)
  Backward   PASS  (4 checked, 0 failures)
  Bidirectional: PASS
  Orphans: none
  Audit report -> output/audit.md, output/audit.csv

Three diagnostic shapes Jama-style:

• forward-fail, backward-pass: a requirement isn't reached by any evidence
• backward-fail, forward-pass: an attestation references evidence that doesn't address the same requirement
• both-fail: both message sets reported, each direction labeled

CLI: uv run python -m traceability.audit --direction {forward|backward|bidirectional|full} --format {csv|md|json}

Persistence Backends

The runtime always builds the Dataset locally. The --backend flag chooses where it ultimately lands:

# (default) write output/rtm.ttl + output/rtm.trig to disk
uv run python -m pipeline.runner --auto --backend=local

# push each named graph to a Flexo MMS instance
uv run python -m pipeline.runner --auto --backend=flexo

# push to a bare Apache Jena Fuseki (no-Flexo fallback)
uv run python -m pipeline.runner --auto --backend=fuseki

The Flexo backend targets the shared remote sandbox at try-layer1.starforge.app by default — see flexo/README.md for the token-based remote workflow and the local Compose-stack alternative.

Audit results are identical across all three backends: the SPARQL queries run against the local Dataset; the backend only persists. Demonstrated live:

=== branches in adcs-demo/lifecycle on starforge ===
attestations  audit  evidence  master  ontology  plan-execution  structural

=== SPARQL triple counts per branch ===
ontology         317       evidence         126
structural       253       attestations      89
plan-execution    52       audit              8

Compute Backends (Phase L)

The Stage 2 / Stage 3 analyses can optionally run inside a Docker container, emulating a remote analysis server. Each container's identity (image digest, container ID, hostname) is captured into the attestation's PROV provenance — so the RTM records where and how each piece of evidence was generated.

make compute-build                                        # one-time image build
uv run python -m pipeline.runner --auto --compute=docker  # remote-emulated compute

Per-activity provenance after a Docker run:

adcs:SA-REQ-003
    prov:atLocation        <urn:adcs:location:docker:71a59f23f3e9> ;
    prov:wasAssociatedWith <urn:adcs:executor:71a59f23f3e9> ;
    prov:startedAtTime     "2026-05-14T02:27:51Z"^^xsd:dateTime ;
    prov:endedAtTime       "2026-05-14T02:27:56Z"^^xsd:dateTime .

<urn:adcs:executor:71a59f23f3e9> a prov:SoftwareAgent ;
    rtm:hostname      "71a59f23f3e9" ;
    rtm:imageDigest   "sha256:92bb8bf18f5f..." ;
    rtm:imageLabel    "adcs-compute:latest" ;
    rtm:containerId   "71a59f23f3e9" ;
    rtm:pythonVersion "3.12.13" .

Image as tracked evidence (WP3)

Under --compute=docker the demo also promotes the image itself to a first-class rtm:DockerImage node in <adcs:evidence> (not just a label on the executor agent). Each Docker-produced evidence node declares prov:wasDerivedFrom <image-iri>, and a SHACL closure rule at Stage 6.5 enforces the link — so the trace can answer "find every evidence node produced by image sha256:…" instead of only "where did this run happen?"

The image node carries six properties:

• rtm:contentHash — runtime image digest (sha256:…)
• rtm:imageLabel — repo:tag
• rtm:baseImageDigest — FROM-image digest resolved at build (may be empty if the base isn't pulled locally; pipeline gracefully degrades)
• rtm:dockerfileHash — SHA-256 of the Dockerfile bytes
• rtm:buildContextHash — SHA-256 over a sorted manifest of build- context file hashes
• prov:generatedAtTime — build timestamp

Reverse lookup helper:

from rdflib import Dataset
from traceability.queries import evidence_by_image

ds = Dataset(default_union=True)
ds.parse("output/rtm.trig", format="trig")
rows = evidence_by_image(ds, "sha256:92bb8bf18f5f...")
# -> [{'ev': 'http://example.org/adcs-demo/EV-PROOF-REQ-003',
#      'type': 'http://example.org/ontology/rtm#ProofArtifact',
#      'evContentHash': '...', 'modelHash': '...'}, ...]

The notebook Act 9 / 10 narrative (showing the image as a node in the rendered trace) + audit-module image surfacing defer to WP5 — WP3 is the backend that makes those narrative passes honest.

Toolchain

What	Required?	Used for
Python 3.12, uv	yes	runtime + tests + ontology build
Docker	optional	--compute=docker Stage 2/3 emulation
OBO ROBOT (Java JAR)	required (default)	make ontology (canonical: Python assembly + ROBOT/ELK verification). No-Java users invoke make ontology-python instead.
FLEXO_TOKEN env var	optional	--backend=flexo live push

uv run python -m pipeline.runner works with no optional tools installed — the runner runs against the committed rtm.ttl. Only rebuilding the ontology with make ontology requires Java + obo-robot.

Ontology Authoring

The canonical artifact ontology/rtm.ttl is built. Edit ontology/rtm-edit.ttl and rebuild:

make fetch-imports     # one-time: pull vendored upstream ontologies
make ontology          # canonical: Python assembly + ROBOT/ELK verification (requires Java + obo-robot)
make ontology-python   # no-Java path: Python assembly only, ROBOT verification skipped
make ontology-robot    # just the ROBOT step (merge + reason + report), without rewriting rtm.ttl

make ontology fails fast when Java or obo-robot are missing; the message points at make ontology-python as the explicit no-Java alternative. The manifest's robot_used flag records which path produced the current artifact; Stage 0's banner is data-driven from that flag.

Every build verifies that each upstream term rtm-edit.ttl references exists in its vendored import, regenerates assembly_manifest.json, and enforces a triple-count budget (TRIPLE_BUDGET=356 in scripts/build_ontology.py) so the integration ontology can't quietly grow novel epistemic vocabulary.

Key Directories

• ontology/ — TBox + shapes + vendored imports + build manifest
• structural/ — SysMLv2 RDF (satellite.ttl, parameters.ttl)
• analysis/ — SymPy proofs + scipy simulation
• evidence/ — content hashing + RDF binding (with execution provenance)
• traceability/ — RTM assembly, queries, attestation, verification, audit
• pipeline/ — stage orchestrator (PipelineState + per-stage functions), Dataset helpers + query_named_graph, plan.ttl, backends
• interrogate/ — explain / reproduce / visualize / rerun
• documents/ — compiled document views over the dataset (DDVS-001)
• compute/ — Local + Docker compute backends + Dockerfile
• flexo/ — Flexo MMS provisioning scripts + live integration docs
• scripts/ — fetch_imports.py + build_ontology.py
• tests/ — 309 tests (306 default run + 3 live-Flexo opt-in) across ontology, named graphs, shapes, audit, backends, compute, document compiler

Future Work

The demo deliberately stops short of several production-grade extensions. Each is documented in the plan file and summarized here so it's easy to pick up:

• Cryptographic envelopes & signatures. Today's hashes are bare SHA-256: content identity but not authenticity. Production should layer W3C VC Data Integrity (Ed25519 over RDF canonicalization), in-toto/SLSA build attestations, and sigstore/Rekor transparency logs.
• Formal authority & credential model. FOAF + W3C Org Ontology + schema:hasCredential + W3C Verifiable Credentials layered on top of prov:Agent — so an attestation records who attested, what role they were authorized in, and what credentials backed that authority.
• OntoGSN confidence arguments. Reify confidence in each Assumption / Justification node so "how confident are you in the adequacy claim?" is a queryable graph instead of prose.
• Defeaters & revocation (SACM-style) — invalidate attestations when later evidence contradicts an earlier assumption.
• Multi-attestation aggregation policy. Sign-off gates (Engineering + QA + Certifier must all attest earl:passed) expressed as SHACL constraints on requirement transitions.
• Production Flexo deployment. Multi-user SSO auth, PR-style branches for RTM evolution, CI hooks, federation across program- level Flexo instances.
• OSLC connector for DOORS Next / Jama / RQM, on top of the alignment axioms already in place.
• Federated SPARQL for cross-program traceability when satellite- and ADCS-level requirements live in different repositories.
• Continuous re-verification in CI plus a live traceability dashboard — both compose with the cryptographic-envelope work.

Acknowledgments

Thanks to Nick (@Nick-phl-7) for feedback and guidance in preparation for the JAXA talk.

License

Apache 2.0 — see LICENSE.