ADCS Lifecycle Demo

Live demo: https://dynamicalsystemsgroup.github.io/ADCS-lifecycle-demo/ Architecture: see ARCHITECTURE.md — the three-remote (git + Flexo + local Docker) + fourth-service (CouchDB txnlog) picture.

Bidirectional requirements traceability for a satellite Attitude Determination and Control System (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>.

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.

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).

AttestationShape — adequacy Assumption + sufficiency Justification + outcome + qualified association
PlanInstantiationShape — every p-plan:Activity corresponds to a known step
EvidenceShape — hashes + source + generating activity + addresses a requirement
RequirementShape — declared name + text
GsnArgumentShape — Goal → Strategy → Solution chain; non-empty statements
ProvenanceShape — Activity has Agent; Entity has ≤1 generating activity
OutcomeSemanticsShape — outcome-specific rationale requirements
ForwardTraceabilityShape / BackwardTraceabilityShape — independent; bidirectional is the conjunction
NamedGraphIntegrityShape — cross-graph references resolve
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
compute/ — Local + Docker compute backends + Dockerfile
flexo/ — Flexo MMS provisioning scripts + live integration docs
scripts/ — fetch_imports.py + build_ontology.py
tests/ — 166 tests across ontology, named graphs, shapes, audit, backends, compute, live Flexo

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.

License

Apache 2.0 — see LICENSE.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Repository files navigation

ADCS Lifecycle Demo

Setup

Core Principle

Architecture

Named-Graph Quadstore Layout

Quick Start

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

Reproducibility verification

Tests

Pipeline Stages

Stage 0 banner (first thing you see)

Pipeline architecture

Interrogation

Rerun plan from a verification report

Requirements

Closure-Rule Suite

Audit (Stage 7a)

Persistence Backends

Compute Backends (Phase L)

Image as tracked evidence (WP3)

Toolchain

Ontology Authoring

Key Directories

Future Work

License

About

Uh oh!

Releases

Packages

Uh oh!

Contributors

Uh oh!

Languages

Name		Name	Last commit message	Last commit date
Latest commit History 92 Commits
.github/workflows		.github/workflows
analysis		analysis
compute		compute
evidence		evidence
flexo		flexo
interrogate		interrogate
ontology		ontology
pipeline		pipeline
scripts		scripts
structural		structural
tests		tests
tools		tools
traceability		traceability
.DS_Store		.DS_Store
.env.example		.env.example
.gitignore		.gitignore
.python-version		.python-version
ARCHITECTURE.md		ARCHITECTURE.md
CLAUDE.md		CLAUDE.md
LICENSE		LICENSE
Makefile		Makefile
README.md		README.md
RECONCILIATION.md		RECONCILIATION.md
docker-compose.yml		docker-compose.yml
main.py		main.py
notebook.py		notebook.py
pyproject.toml		pyproject.toml
uv.lock		uv.lock

Folders and files

Latest commit

History

Repository files navigation

ADCS Lifecycle Demo

Setup

Core Principle

Architecture

Named-Graph Quadstore Layout

Quick Start

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

Reproducibility verification

Tests

Pipeline Stages

Stage 0 banner (first thing you see)

Pipeline architecture

Interrogation

Rerun plan from a verification report

Requirements

Closure-Rule Suite

Audit (Stage 7a)

Persistence Backends

Compute Backends (Phase L)

Image as tracked evidence (WP3)

Toolchain

Ontology Authoring

Key Directories

Future Work

License

About

Topics

Resources

License

Uh oh!

Stars

Watchers

Forks

Releases

Packages 0

Uh oh!

Contributors

Uh oh!

Languages

Packages