Chapter 10: Traceability and Sign-off¶
Purpose¶
This chapter builds a real traceability graph over two of the model’s three named requirements, synthesizes three of the tutorial’s own real judgment records into a ledger, and assembles the real inputs a real sign-off decision would be made from: a bounded, honest synthesis of what is established, what is not, and what residual judgment remains. This chapter does not perform that sign-off itself, and does not claim to: deciding whether to proceed remains a human, accountable act. This is the tutorial’s final chapter.
This chapter adds exactly one new named model element, and only because its own traceability analysis finds a real gap it is positioned to close directly: otherwise, models/ch10-cumulative.sysml carries models/ch08-cumulative.sysml’s content forward unchanged, the same deliberate design choice Chapter 9 made. This is not a departure from that design principle in general: the one exception is warranted precisely because it is not new model content for its own sake, it is the direct result of what this chapter’s own traceability graph discovered (notebook 01 finds deliveredEnergyBoundedBySupply, Chapter 8’s own Z3-proved conservation lemma, tied to no requirement at all, then closes that gap by subsetting it directly from EnergyConservationReq’s own required constraint -- deliberately with no assert satisfy line; see the case study and notebook 01’s own AC-C10 for why). Unlike Chapter 9, this chapter commits its own models/ch10-cumulative.sysml file: Chapter 9 left no cumulative fixture of its own, which would have made scripts/check_construction.py’s own predecessor-containment check silently no-op between Chapter 8 and Chapter 10. This chapter resolves that for real: check_predecessor_containment() now falls back to the nearest earlier chapter with a real fixture when the immediate predecessor has none, so Chapter 8’s own named elements are actually checked against this chapter’s own committed file, not skipped.
Ingredients¶
| Notebook | Concept |
|---|---|
| 01: traceability graph | Trace two of the model’s three requirements from functional intent through allocation and realization to verification evidence, built entirely from real queries; find that the model’s own strongest formal proof is tied to no requirement at all, close that gap directly by subsetting (not by assert satisfy, confirmed by negative control to fail, across three different bindings), and record how that tie should honestly be read (AC-C10). |
| 02: judgment ledger | Reconstruct AS-C06 and AS-C08 (re-verified against their real originals) plus AI-C06, and read what each record’s own kind, disposition and residual uncertainty actually says. |
| 03: engineering synthesis | Synthesize the graph and the ledger into one honest, bounded record, and state plainly why that record is not itself sign-off. |
Equipment¶
See Getting Started for environment setup. No additional tooling beyond earlier chapters.
Method¶
Notebook 01 finds each requirement’s own declared subject by reading the requirement definition’s own subject feature in the API-JSON export, then follows the real allocation and realization chain to each one’s physical candidates, and joins that chain against requirement_coverage()'s own polarity-correct result (Chapter 9). heatGenerationReq traces all the way to genuine, opposite-polarity evidence (rated satisfies it, weak fails it); timely traces just as far through intent, allocation and realization, but stops one link short, since no candidate has ever been positively checked against it. The notebook also asks the same question in the other direction: is deliveredEnergyBoundedBySupply, the one property in this tutorial proved by Z3 for every value its unbound features admit, tied to any requirement usage at all? Before this chapter’s own remediation, it was not: the inverse of a failure mode Douglas’s own traceability concern names (an unjustified widget, a design element with no requirement behind it), here evidence disconnected from any stated need instead. The notebook closes that gap directly: EnergyConservationReq/energyConservationReq restates the lemma’s own property as a stakeholder-facing requirement, with no explicit subject line (its own required constraint never references a subject at all, so declaring one would commit to an arbitrary, unused type; the requirement inherits RequirementCheck’s own default subject, Anything, the honest reflection of that -- SysML v2 formal/2026-03-02 SS7.21.1), and its own require constraint c :> deliveredEnergyBoundedBySupply; ties the lemma to it from within the requirement’s own body -- confirmed by requirement_ties() before and after. Deliberately absent is an assert satisfy line: a negative control in the same notebook shows that construct makes model.verify_satisfaction() error identically regardless of its own binding, because this requirement’s own required constraint never references its subject at all. AC-C10, an asserted_context judgment record, then frames honestly how this tie should be read: the subsetting mechanism is spec-legitimate and the requirement’s own general motivation is genuine, but its own need was identified retroactively to close this chapter’s own traceability gap, and the tie rests on structural detection alone (requirement_coverage()‘s own covered=False for it is correct and expected, not a residual gap). Notebook 02 reconstructs three real judgment records verbatim, AS-C06 and AS-C08 (already reconstructed once by Chapter 9, re-verified here rather than assumed correct) plus AI-C06 (Chapter 6’s own stopping judgment, an asserted_inference, alongside the two asserted_solution records), and reads each one’s own kind, disposition and residual uncertainty rather than only its count. Notebook 03 synthesizes both into one new record, AI-C10, an asserted_inference whose own premises are literally the other two notebooks’ findings, and states explicitly why that record, however honest and however carefully bounded, is not sign-off itself.
Expected result¶
After running all three notebooks: notebook 01’s graph shows heatGenerationReq covered on both sides (satisfied_by=['rated'], failed_by=['weak']), timely covered one-sidedly, a negative claim only (satisfied_by=[], failed_by=['slow']), and deliveredEnergyBoundedBySupply, found tied to no requirement usage, closed by this same notebook’s own remediation and now tied to EnergyConservationReq by subsetting (energyConservationReq itself reports covered=False, by design, with AC-C10 validating cleanly and keeping disposition="pending"/engineering_conclusion="undetermined"); notebook 02’s ledger shows three records, all disposition="pending" and record_kind="worked_example", two engineering_conclusion="undetermined" (AS-C06, AI-C06) and one "supported" but narrowly scoped (AS-C08); notebook 03’s synthesis record (AI-C10) validates cleanly, keeps disposition="pending" and engineering_conclusion="undetermined", and the notebook states plainly, in prose, that this record is not sign-off.