{
  "id": "page:library-composition-aerospace-flight-control",
  "_kind": "Page",
  "_file": "wiki/library/composition-aerospace-flight-control.md",
  "_cluster": "wiki",
  "attributes": {
    "nodeKind": "Page",
    "title": "Composition: Aerospace Flight Control (Waterfall + V-Model + Cleanroom + inline Formal Verification) (Library)",
    "displayName": "Composition: Aerospace Flight Control (Waterfall + V-Model + Cleanroom + inline Formal Verification) (Library)",
    "slug": "library/composition-aerospace-flight-control",
    "articlePath": "wiki/library/composition-aerospace-flight-control.md",
    "article": "\n# Composition: Aerospace Flight Control (Waterfall + V-Model + Cleanroom + inline Formal Verification)\n\nDO-178C flight-control software archetype: Waterfall system/software requirements\ncapture, V-Model decomposition with per-level verification plans, Cleanroom\nincremental development with statistical usage testing, **inline** formal\nverification of critical properties (parallel per-property proofs with\n**executed** proof-checker output), certification evidence assembly behind an\nindependent adversarial certification gate, and a policy-gated flight-software\nbaseline release. Every stage exit is guarded by an **executed**\nrequirement-to-verification traceability gate plus a routed verification-lead\nsign-off; safety-requirement waivers, DER certification sign-off, and baseline\nrelease are **fail-closed** policy-gated approvals that never auto-execute.\n\nImplements `library/methodologies/backlog.md` Example 6 (line 2183, previously\n*Not Implemented*). Pairs with `composition-regulated-greenfield` to complete\nthe **safety / compliance quadrant** of the methodology matrix.\n\n## Why this composition\n\nEach ingredient contributes a distinct DO-178C capability:\n\n- **Waterfall** — staged rigor and the frozen, sign-off-gated document sequence\n  certification authorities audit (system/software requirements capture).\n- **V-Model** — every left-side design artifact is paired with its right-side\n  test level, making requirement-to-verification traceability *computable* and\n  giving each level its own DO-178C verification plan (independence + structural\n  coverage objectives).\n- **Cleanroom** — defect prevention through box-structure formal specification\n  and statistical certification of reliability over an operational usage model.\n- **Formal Verification** — machine-checkable proofs for the critical properties\n  (safety invariants, control-loop timing/liveness, numerical stability) that\n  testing alone cannot certify to Level A confidence.\n\n## Inline formal verification (missing-ingredient rationale)\n\nThere is **no** `library/methodologies/formal-verification/` directory in the\nlibrary. Rather than reference a nonexistent dir or skip the ingredient, the\nformal-verification methodology is modeled **inline** as first-class `caf.formal-*`\ntasks inside this composition, following the **batch-3 strangler-fig precedent**\nestablished by `composition-legacy-modernization` (which models legacy-modernization\nstrangler-fig behavior inline the same way).\n\nThe inline seam is deliberately extraction-ready. A future standalone\n`formal-verification` methodology dir can lift, unchanged:\n\n- the task set `caf.formal-property-extraction` -> `caf.formal-model-construction`\n  -> `caf.property-proof` (executed) -> `caf.fix-formal` (counterexample-driven),\n- the `caf.formal.proof-audit` adversarial gate, and\n- the **proof-evidence schema**\n  `artifacts/caf/formal/<propertyId>/proof-output.json`\n  `{propertyId, proofStatus, executionRecord{statesExplored|obligationsDischarged, bound, wallTime}, counterexample|null}`.\n\nThis kip fact records the seam:\n`process:composition-aerospace-flight-control --inlines-methodology--> methodology:formal-verification`\nwith `props.seam = 'caf.formal-* task set + proof-evidence schema'`.\n\n## Phase flow\n\n```mermaid\nflowchart TD\n  P0[Phase 0: kip recall] --> P1\n  P1[Phase 1: Waterfall requirements + safety assessment] --> P2\n  P2[Phase 2: V-Model decomposition + per-level verification plans] --> P3\n  P3[Phase 3: Cleanroom increments + statistical usage testing] --> P4\n  P4[Phase 4: INLINE formal verification of critical properties] --> P5\n  P5[Phase 5: V-Model right-side verification] --> P6\n  P6[Phase 6: Certification evidence + independent gate + DER sign-off] --> P7\n  P7[Phase 7: Flight-software baseline release] --> P8\n  P8[Phase 8: kip assert]\n\n  P1 -. certifiedStageExit .-> G1{{caf.requirements.traceability}}\n  P2 -. certifiedStageExit .-> G2{{caf.decomposition.traceability}}\n  P3 -. certifiedStageExit .-> G3{{caf.cleanroom-development.traceability}}\n  P4 -. proof-audit .-> GF{{caf.formal.proof-audit}}\n  P4 -. certifiedStageExit .-> G4{{caf.formal-verification.traceability}}\n  P5 -. per-level .-> GV{{caf.verification.unit|integration|system|acceptance}}\n  P5 -. certifiedStageExit .-> G5{{caf.verification.traceability}}\n  P6 -. independent .-> GC{{caf.certification.evidence}}\n```\n\nPhases are strictly sequential. `ctx.parallel.all` is used only **within** a\nphase:\n\n- **Phase 2** — per-level verification planning (four V-Model levels) and per-module module design.\n- **Phase 4** — per-property formal analysis (model construction -> executed proof -> bounded fix).\n- **Phase 5** — per-module (unit) and per-suite (integration) work; the four verification **levels** are sequential.\n- **Phase 3** increments are deliberately **sequential** — Cleanroom increments build on prior increments.\n\n## Ingredients composed by name\n\nIngredient `process()` functions are **not** called — only exported `defineTask`\ntasks are composed, so ingredient-internal breakpoints/loops never double-fire.\n\n| Task | Source module | Phase |\n| --- | --- | --- |\n| `requirementsGatheringTask` | `../waterfall/waterfall.js` | 1 |\n| `requirementsWithAcceptanceTask` | `../v-model/v-model.js` | 1 |\n| `systemDesignWithSystemTestTask` | `../v-model/v-model.js` | 2 |\n| `architectureWithIntegrationTestTask` | `../v-model/v-model.js` | 2 |\n| `moduleDesignWithUnitTestTask` | `../v-model/v-model.js` | 2 (parallel per module) |\n| `executeTestsTask` | `../v-model/v-model.js` | 5 (per level/scope) |\n| `traceabilityMatrixTask` | `../v-model/v-model.js` | every stage exit + 6 |\n| `planIncrementsTask` | `../cleanroom/cleanroom.js` | 3 |\n| `createFormalSpecificationTask` | `../cleanroom/cleanroom.js` | 3 (per increment) |\n| `designWithVerificationTask` | `../cleanroom/cleanroom.js` | 3 (bounded fix loop) |\n| `fixDesignTask` | `../cleanroom/cleanroom.js` | 3 (fix-loop body) |\n| `implementIncrementTask` | `../cleanroom/cleanroom.js` | 3 |\n| `codeInspectionTask` | `../cleanroom/cleanroom.js` | 3 (bounded fix loop) |\n| `fixImplementationTask` | `../cleanroom/cleanroom.js` | 3 (fix-loop body) |\n| `createUsageModelTask` | `../cleanroom/cleanroom.js` | 3 (statistical) |\n| `generateStatisticalTestsTask` | `../cleanroom/cleanroom.js` | 3 (statistical) |\n| `executeStatisticalTestsTask` | `../cleanroom/cleanroom.js` | 3 (executed) |\n| `analyzeReliabilityTask` | `../cleanroom/cleanroom.js` | 3 (statistical) |\n\nCombinators (`routedBreakpoint`, `adversarialGate`, `kipRecall`, `kipAssert`)\nare imported from\n`../../specializations/common-utilities/routed-gate-combinators.js` — never\nre-implemented.\n\nLocal `caf.*` tasks (all `kind: 'agent'`): `caf.safety-assessment`,\n`caf.level-verification-plan`, `caf.trace-diff`, `caf.formal-property-extraction`,\n`caf.formal-model-construction`, `caf.property-proof`, `caf.fix-formal`,\n`caf.fix-verification`, `caf.assemble-certification-evidence`,\n`caf.baseline-release`.\n\n### Task-registry collision\n\n`waterfall.js` and `v-model.js` both register the task id `implementation` at\nmodule-evaluation time (a known library-wide shared-id issue). This composition\nuses **neither** module's `implementation` task — Cleanroom's\n`implementIncrementTask` does implementation — so the two modules are imported\nsequentially via top-level `await import(...)`, and the inert colliding\ndefinition is cleared between them (the same pattern as\n`composition-regulated-greenfield`).\n\n## Policy-gated actions (adapters/policy ready)\n\n`breakpointId === actionId` exactly; none carries `autoApproveAfterN` or\n`presentAlwaysApprove`; every decision records `autoApproved: false` provenance.\n\n| actionId (== breakpointId) | Expert | When raised | Fail-closed semantics |\n| --- | --- | --- | --- |\n| `requirement-waiver-approval` | certification-liaison | By `requireSafetyWaiver` for ANY deviation from a captured safety requirement or DO-178C objective (refuted hinted requirements, unformalizable critical properties, exhausted proof/fix budgets, reliability/coverage shortfalls) | **NEVER** auto-executes; rejection **throws**; approvals appended per-requirement to the waivers provenance log, never generalized |\n| `certification-evidence-signoff` | designated-engineering-representative | Phase 6, only **after** the independent `caf.certification.evidence` gate passed; payload structurally requires the executed gate result + evidence index | **NEVER** auto-executes; rejection **throws** — the package cannot be released unsigned |\n| `flight-software-baseline-release` | chief-engineer | Phase 7 | **NEVER** auto-executes; guarded executor `caf.baseline-release` runs **only** on `approved === true`; rejection leaves `baselineRelease` null and `success` false — no fallback |\n\n**Process breakpoints** (not policy-gated actions): `caf.stage-exit.<stage>`\n(verification-lead, one per stage exit: requirements, decomposition,\ncleanroom-development, formal-verification, verification) and failure-only owner\nescalations (`caf.phase-3.design-escalation.<increment>`,\n`caf.phase-3.inspection-escalation.<increment>`,\n`caf.phase-5.<level>-escalation.<scope>`). Owner acceptance of a shortfall\ntouching a safety requirement **additionally** requires\n`requirement-waiver-approval` — owner escalation never substitutes for the\ncertification-liaison waiver.\n\n## Stage-exit contract (`certifiedStageExit`)\n\n1. **Executed traceability** — `traceabilityMatrixTask` computes the stage\n   matrix; `caf.trace-diff` diffs it against the previous stored matrix + the SRS\n   requirement set, writing `artifacts/caf/<stage>/trace-diff.json`.\n2. **Adversarial gate** — `adversarialGate` (`gateId: caf.<stage>.traceability`)\n   over the executed diff with `traceability-critic` + `waiver-provenance-critic`,\n   IRON LAW (\"re-run the trace computation or cite the executed trace-diff.json\n   line-by-line\"), bounded fixer, owner escalation. Gate failure throws.\n3. **verification-lead sign-off** — `routedBreakpoint` with the per-stage-unique\n   `caf.stage-exit.<stage>` id; payload built from the executed gate result after\n   a structural malformed-check, so sign-off without traceability evidence is\n   impossible to construct.\n4. **Rejected sign-off throws** — stages are sequential, no skip-ahead.\n\n## Gate catalog and evidence schemas\n\n| Gate | Reviews | Evidence schema |\n| --- | --- | --- |\n| `caf.<stage>.traceability` (x5) | executed trace diff | `artifacts/caf/<stage>/trace-diff.json` `{stage, coveredCount, uncovered, orphanedVerifications, regressions, waivedRequirements[{reqId, waiverBreakpointEventId}]}` |\n| `caf.formal.proof-audit` | executed proof outputs | `artifacts/caf/formal/<propertyId>/proof-output.json` `{propertyId, proofStatus, executionRecord{statesExplored|obligationsDischarged, bound, wallTime}, counterexample|null}` |\n| `caf.verification.<level>` (x4) | executed test runs | `artifacts/caf/verification/<level>/results.json` (executed test-run results per plan method) |\n| `caf.certification.evidence` | assembled evidence index | `artifacts/caf/certification/evidence-index.json` `{sections[{objective, artifactPath|breakpointEventId}], openItems}` |\n\nThe certification gate is **independent and adversarial**: `certification-auditor`\n+ `evidence-integrity-critic` are distinct from all producer roles **and** from\nevery per-stage critic; the auditor must SPOT-CHECK by re-executing at least one\ntest level and one property proof and diffing against recorded outputs. Every\ngate reviews **executed** artifacts — never prose.\n\n## Inputs\n\n| Input | Type | Default |\n| --- | --- | --- |\n| `systemRequirements` | `string` | **REQUIRED** — empty throws |\n| `dalLevelHint` | `string` | — (hint only; `caf.safety-assessment` is authoritative) |\n| `flightControlFunctions` | `string[]` | `[]` |\n| `criticalPropertiesHint` | `string[]` | `[]` (hint only) |\n| `complianceStandards` | `string[]` | `['DO-178C']` |\n| `incrementCountHint` | `number` | — (hint only) |\n| `kipDir` | `string` | `.a5c/kip` |\n| `kipModel` | `string` | `sonnet` |\n| `maxFixAttempts` | `number` | `2` |\n| `maxProofAttempts` | `number` | `2` |\n\n## Outputs\n\n`{ success, srs, safetyAssessment, vModelDesign, cleanroomDevelopment, formalVerification, verification, traceabilityMatrices, waivers, certificationEvidence, signoffs, baselineRelease, metadata }`\n\n- `baselineRelease` is `null` and `success` is `false` whenever the\n  `flight-software-baseline-release` breakpoint is rejected — no fallback path.\n- `verification` is keyed by level (`unit` / `integration` / `system` /\n  `acceptance`) plus `levelGates`.\n- `waivers` is the full safety-requirement waiver provenance log; each entry\n  records `{breakpointEventId, breakpointId, requirementIds, rationale, requestingStage, approvedAt, respondedBy, autoApproved:false}`.\n\n## Exported tasks and helpers\n\n| Export | Kind | Role |\n| --- | --- | --- |\n| `safetyAssessmentTask` | task | Authoritative DO-178C software-level assignment + critical properties |\n| `levelVerificationPlanTask` | task | Per-V-Model-level verification plan (independence + coverage) |\n| `traceDiffTask` | task | Computed requirement->verification set-diff (waiver provenance) |\n| `formalPropertyExtractionTask` | task | Inline formal step 1: property set |\n| `formalModelConstructionTask` | task | Inline formal step 2: per-property model |\n| `propertyProofTask` | task | Inline formal step 3: EXECUTED proof check |\n| `fixFormalTask` | task | Counterexample-driven proof fixer / proof-audit gate fixer |\n| `fixVerificationTask` | task | V-Model verification-level fixer / level-gate fixer |\n| `assembleCertificationEvidenceTask` | task | DO-178C evidence index assembly / certification-gate fixer |\n| `baselineReleaseTask` | task | Guarded executor: cut the flight-software baseline |\n| `requireSafetyWaiver` | helper | Fail-closed policy-gated waiver guard |\n| `certifiedStageExit` | helper | Stage-boundary contract (executed trace + gate + sign-off) |\n| `process` | orchestrator | `process(inputs, ctx)` |\n\n## Usage\n\n```bash\nbabysitter run:create \\\n  --process library/methodologies/composition-aerospace-flight-control/composition-aerospace-flight-control.js \\\n  --input '{\"systemRequirements\": \"Fly-by-wire primary flight control: pitch/roll/yaw command laws with triple-redundant actuators, envelope protection, and a 20ms control-loop deadline. DO-178C Level A.\", \"flightControlFunctions\": [\"pitch-law\", \"roll-law\", \"envelope-protection\"], \"criticalPropertiesHint\": [\"actuator-command-bounds\", \"control-loop-deadline\", \"mode-exclusion\"]}'\n```\n\n## Relationship to ingredients and to composition-regulated-greenfield\n\nThis composition and `composition-regulated-greenfield` together fill the\nsafety/compliance quadrant. `composition-regulated-greenfield` targets a\nHIPAA-regulated greenfield build (Waterfall + DDD + Cleanroom + V-Model with\nPHI-access policy gating); this one targets a DO-178C flight-control build,\nswapping DDD for **inline formal verification** and adding the certification\nevidence package + baseline release. Both share the same backbone:\ncombinator-based routed breakpoints and adversarial gates, an executed-trace\nstage-exit contract, guarded policy-gated executors, per-item waiver/approval\nprovenance threading, and kip recall/assert (here under kind\n`methodology-composition`). The `caf.formal-*` seam documented above is the\nextraction point should formal verification become a standalone methodology dir.\n",
    "documents": [
      "specialization:composition-aerospace-flight-control"
    ]
  },
  "outgoingEdges": [
    {
      "from": "page:library-composition-aerospace-flight-control",
      "to": "specialization:composition-aerospace-flight-control",
      "kind": "documents"
    }
  ],
  "incomingEdges": [
    {
      "from": "page:index",
      "to": "page:library-composition-aerospace-flight-control",
      "kind": "contains_page"
    }
  ]
}