Skip to content

CLAUDE.md

Latest commit

 

History

History
321 lines (263 loc) · 15.5 KB

CLAUDE.md

File metadata and controls

321 lines (263 loc) · 15.5 KB
Raw

ADCS Lifecycle Demo

What this is

A demonstration of bidirectional requirements traceability for a satellite Attitude Determination and Control System (ADCS). The demo traces the full lifecycle from SysMLv2 structural specification through symbolic analysis (SymPy), numerical simulation (scipy), and human expert attestation — with all traceability stored as RDF in a named-graph quadstore and all artifacts version-controlled in git.

Core principle

Evidence does not verify requirements; evidence supports a human judgment that requirements are satisfied. Models are imperfect representations of physical systems. The engineer judges model adequacy and evidence sufficiency. Only human attestation connects evidence to requirement satisfaction.

This split is the Hawkins–Habli Assurance Claim Point categorization: adequacy is a gsn:Assumption, sufficiency is a gsn:Justification. The project's rtm: namespace introduces NO novel epistemic vocabulary.

Architecture — integration ontology

rtm: is a thin application/integration ontology. Convenience classes and properties are subclasses / subproperties of established standards; the project's contribution is the assembly, not new terms.

Namespace Role
prov: Provenance spine
sysml: ↔ omg-sysml: SysMLv2; local prefix aliased to OMG SysMLv2 OWL
earl: Assertion + outcome lattice + mode
gsn: (OntoGSN) Goal / Strategy / Solution / Assumption / Justification
p-plan: Process model (one Step per pipeline stage)
oslc_rm: / oslc_qm: Tool-interop aliases for RM tools
sh: SHACL closure-rule suite

Named-graph layout (rdflib.Dataset)

The runtime is Dataset(default_union=True) so SPARQL queries match across named graphs without GRAPH clauses. Each layer lives in its own graph, sized to match Flexo MMS branch conventions:

<rtm:ontology>        TBox + shapes + individuals
<rtm:plan>            P-PLAN process model
<adcs:structural>     SysMLv2 instance data
<adcs:context>        Stable gsn:Context / gsn:Assumption individuals
<adcs:evidence>       rtm:Evidence artifacts (incl. rtm:DockerImage under --compute=docker, WP3)
<adcs:attestations>   rtm:Attestation events
<adcs:plan-execution> p-plan:Activity instances (one per stage)
<adcs:audit>          Forward/backward/bidirectional audit summary

IRIs and the NAMED_GRAPHS dict are in ontology/prefixes.py.

Three-remote architecture (WP4)

The demo runs against three remotes + a fourth service. See ARCHITECTURE.md for the full picture; one-paragraph summary:

  • git holds code, ontology, Dockerfile.
  • Flexo holds RDF named graphs (incl. rtm:DockerImage records).
  • local Docker is the runtime: image (static, content-addressed) vs container (transient, per-run) vs host (the machine).
  • transaction-log store (CouchDB; opt-in via ADCS_TXNLOG_ENABLED=1) holds the wire-log JSON for each service invocation.

URI scheme (canonical shapes):

  • Image: urn:adcs:docker-image:<digest> (rtm:DockerImage)
  • Container: urn:adcs:docker-container:<container-id> (rtm:DockerContainer)
  • Host: urn:adcs:location:docker:<host> (prov:Location)
  • Executor: urn:adcs:executor:<id> (prov:SoftwareAgent)
  • Operating org: urn:adcs:org:local-operator default (prov:Organization)
  • Flexo record: urn:adcs:flexo:<org>/<repo>/<branch>
  • Flexo service: urn:adcs:service:flexo-mms
  • Txnlog service: urn:adcs:service:transaction-log-store

Standard PROV edges link them: <container> prov:wasDerivedFrom <image>, <activity> prov:used <container>, <executor> prov:actedOnBehalfOf <operating-org>. Auspices are per substrate: each substrate's location/service node carries rtm:operatedBy (subPropertyOf prov:wasAttributedTo) pointing at its OWN hosting org — the compute host gets ADCS_HOSTING_ORG_* (defaults to the operating org), the Flexo service node gets ADCS_FLEXO_HOSTING_ORG_*, the txnlog service node gets ADCS_TXNLOG_HOSTING_ORG_* (defaults to the compute hosting org). FLEXO_ORG is the Flexo MMS org slug (REST path segment), not an auspices IRI. The image carries rtm:gitRef + rtm:flexoRecord for cross-remote linking; the record links prov:atLocation to the service node.

EARL-wrapped verification outcomes sit beside human attestation: rtm:ClosureRuleAssertion (Stage 6.5 SHACL outcome), rtm:DigestMatchAssertion (compute.reproduce rebuild outcome), and rtm:BehaviorOracleAssertion (analysis.oracle metric-vs-criterion outcome) are all earl:Assertion subclasses with earl:mode = earl:automatic. The behavior oracle verifies a model-level claim (a computed metric against a requirement's machine-readable acceptance criterion); it never asserts physical requirement satisfaction — that remains human attestation only. Accordingly it links the requirement via rtm:evaluatesAgainst (subPropertyOf prov:used), never rtm:attests.

Preflight gate probes every configured backend before Stage 0 and fails fast on any unreachable remote. Matches WP2's ROBOT-default discipline — no silent degrade.

Seven trust queries in traceability/queries.py answer "how can I trust this?" — technical_provenance, auspices_chain, reproducibility_witnesses, closure_witnesses, service_invocations_for, service_auspices, trust_summary.

Key directories

  • ontology/ — rtm-edit.ttl (source), rtm.ttl (built artifact), rtm_shapes.ttl (closure-rule suite), rtm_individuals.ttl, sysml_term_map.csv, assembly_manifest.json, imports/ (vendored upstreams)
  • structural/ — SysMLv2 RDF model
  • analysis/ — SymPy symbolic analysis + scipy numerical simulation + traceable behavior-model oracle (oracle.py)
  • compute/ — LocalCompute (in-process) + DockerCompute (containerized remote-emulation with PROV provenance capture) + Dockerfile
  • evidence/ — content hashing + RDF evidence binding (with execution metadata)
  • traceability/ — RTM assembly, SPARQL queries, attestation (GSN-based), closure-rule verification (verification.py), behavior-oracle assertion emitter (oracle_assertion.py), audit module
  • pipeline/ — stage orchestrator (PipelineState + per-stage free functions in runner.py; state.py defines the typed result records), dataset.py (named-graph helpers incl. query_named_graph), stage0_assembly.py, plan.ttl, backends/ (Local / Flexo / Fuseki)
  • flexo/ — Flexo MMS provisioning scripts + integration docs
  • interrogate/ — explain / reproduce / visualize / rerun
  • documents/ — compiled document views over the dataset (design_description.py builds DDVS-001; deterministic, never hand-edited)
  • scripts/ — fetch_imports.py, build_ontology.py
  • tests/ — 309 tests: 306 in the default run + 3 live-Flexo opt-in (alignment, named graphs, shape suite, audit, backends, compute, behavior oracle, document compiler)

Pipeline (stages 0–8)

Stage 0 narrates the ontology assembly; Stage 6.5 runs the closure-rule suite; Stage 7a runs the audit. Every stage emits a p-plan:Activity into <adcs:plan-execution> so the construction process is itself queryable.

Pipeline state + structured stage results

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 (StructuralResult, SymbolicResult, NumericalResult, …) that the next stage reads via state.<prior>.<field>. The runner's job is narration + the ordered call sequence; stage bodies stand alone and are unit-testable.

PipelineState.activity_to_stage maps p-plan step IRI fragments (STEP_NAMES in traceability/plan_execution.py) to stage numbers; interrogate/rerun.py keeps a parallel ACTIVITY_TO_STAGE table, cross-checked by a unit test against STEP_NAMES.

CLI surface

Every CLI in this repo is a Typer app (Click + Rich transitively). Pattern per module: app = typer.Typer(...) + @app.command() function + if __name__ == "__main__": app(). Existing uv run python -m <module> invocations and the [project.scripts] adcs-pipeline console script work unchanged. Choice-validated options use Enum subclasses so Typer matches the prior argparse choices= semantics.

CLIs today:

  • pipeline.runner — runs the full lifecycle (flags: --auto, --no-attest, --engineer, --rebuild, --backend, --compute).
  • interrogate.rerun — translates a verification report into the pipeline stages that must re-run (flags: --input, --requirement, --format).
  • documents.design_description — compiles DDVS-001, a deterministic Markdown design-description/VCRM view over output/rtm.trig (flags: --input, --output, --requirement, --check, --stdout). Byte-identical rebuilds: document date = MAX(prov:generatedAtTime) (never wall clock), fingerprint = sha256 of the raw input file bytes (bnode relabeling rules out re-serialization hashing); --check is the drift gate.

interrogate.explain, interrogate.reproduce, interrogate.visualize are library-only (no CLI entry points). Tests use typer.testing.CliRunner in tests/test_cli.py. A top-level adcs aggregator (adcs pipeline run, adcs interrogate rerun, etc.) is tracked as a follow-up — see issue #5.

Verification vs validation (term discipline)

Strict semantic split across module names, function names, doc strings, RDF property labels, log/banner strings, and commit messages:

  • Verification = automated check whose computation result is fully specified (SHACL conformance, ROBOT/ELK consistency, content-hash matching, completeness checks, HTTP-connectivity probes, triple-count budgets, behavior-oracle metric-vs-criterion comparison in analysis.oracle).
  • Validation = human judgement with expertise, additional context, and/or interpretation (engineer attestation, adequacy assumption, sufficiency justification).

This breaks with pyshacl's validate() convention deliberately — upstream APIs keep their names, the demo's own wrappers use the discipline. SHACL conformance is wrapped by traceability.verification.verify; human judgement lives in traceability.attestation.request_attestation. The split pairs with the longer-standing rule that evidence does not verify requirements; only human attestation does: evidence and verification are both system-internal, attestation is the human boundary.

One IRI fragment is intentionally out-of-sync with the discipline: <plan/step/ValidateShapes> in pipeline/plan.ttl is preserved so already-persisted <adcs:plan-execution> and <adcs:audit> graphs stay valid. The rdfs:label says "Verify"; the IRI rename is tracked separately for a future Flexo migration.

Toolchain

  • Python 3.12+, managed by uv — required
  • rdflib for RDF/SPARQL, sympy for symbolic math, scipy for ODE integration
  • pyshacl for closure-rule verification (the demo's own wrapper is named verify; pyshacl's upstream API is validate and is wrapped, not renamed), httpx for backend HTTP, typer for CLI surfaces
  • ProofScript/ProofBuilder pattern reimplemented from gds-proof
  • Docker — optional, for --compute=docker
  • OBO ROBOT (Java) — required for default make ontology; no-Java users invoke the explicit make ontology-python target instead. CI installs Java 17 + a cached robot.jar and verifies every push.

Running

uv run python -m pipeline.runner --auto            # local backend, local compute
uv run python -m pipeline.runner --auto --backend=flexo   # push to Flexo MMS
uv run python -m pipeline.runner --auto --compute=docker  # remote-compute emulation

The runner runs against the committed rtm.ttl; it does NOT need Java/obo-robot. Only rebuilding the ontology does.

Tests

uv run pytest               # default: skips live + network markers
uv run pytest -m live       # opt-in: live Flexo MMS round-trip (needs FLEXO_TOKEN)
uv run pytest -m network    # opt-in: reserved for W3C-vocab fetches

Marker filtering is set in pyproject.toml via addopts = "-m 'not live and not network'". tests/test_flexo_live.py carries the live marker; tests there fail loudly when -m live is requested without credentials rather than silently skipping (skip-on-opt-in would hide infra breakage).

Ontology rebuild

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 (no rtm.ttl rewrite)

make ontology fails fast on missing Java/obo-robot. The no-Java escape is the explicit ontology-python target — invoking it is an intentional opt-out, not a flag. The manifest's robot_used field + Stage 0 banner record which path produced the artifact. The build also enforces a triple-count budget (TRIPLE_BUDGET=356 in scripts/build_ontology.py) so the integration ontology can't quietly grow novel epistemic vocabulary.

rtm.ttl is a built artifact. Edit rtm-edit.ttl and rebuild.

Commit rtm-edit.ttl BEFORE you rebuild rtm.ttl. rtm.ttl's # Built <time> stamp comes from _reproducible_build_time(), which reads the git commit time of rtm-edit.ttl. Rebuilding while that edit is still uncommitted stamps the previous commit's time, so the committed rtm.ttl won't match CI's rebuild and the CI git diff --exit-code -- ontology/rtm.ttl check fails (ROBOT/ELK itself still passes). Order: commit rtm-edit.ttl → make ontology → commit rtm.ttl + assembly_manifest.json.

Local toolchain (macOS): the brew JDK + obo-robot aren't found by /usr/bin/java or /usr/libexec/java_home, so point JAVA_HOME at the Homebrew openjdk and put obo-robot on PATH:

JAVA_HOME=/opt/homebrew/opt/openjdk PATH="/opt/homebrew/bin:$PATH" make ontology   # Apple Silicon

The Makefile now auto-detects /opt/homebrew vs /usr/local for JAVA_HOME.

Future work (priority order)

Captured in the plan file at /Users/z/.claude/plans/i-want-to-look-hidden-balloon.md:

  1. Cryptographic envelopes & signatures — W3C VC Data Integrity (eddsa-rdfc-2022) + in-toto/SLSA + sigstore/Rekor. Today's bare SHA-256 gives content identity, not authenticity.
  2. Formal authority/credential model — FOAF + Org Ontology + schema:hasCredential + W3C Verifiable Credentials on top of prov:Agent.
  3. OntoGSN confidence arguments — reify per-ACP confidence.
  4. Defeaters & revocation (SACM-style).
  5. Multi-attestation aggregation policy — sign-off gates as SHACL.
  6. Production Flexo deployment — multi-user auth, PR branches for RTM evolution, federation.
  7. OSLC connector for DOORS Next / Jama / RQM.
  8. Federated SPARQL for cross-program traceability.
  9. Continuous re-verification in CI + live traceability dashboard.

Notebook Act 9–10 demonstrate the capture side of remote compute provenance. Production replay against a pulled image is a future addition that pairs with item #1.