Chapter 10 Conclusion¶
What we built¶
One new model element, and only because this chapter’s own analysis found the gap it closes: models/ch10-cumulative.sysml otherwise carries models/ch08-cumulative.sysml’s content forward unchanged, and every notebook in this chapter queries it directly. What changed is what can be asked of it and of the tutorial’s own record set: notebook 01 adds a real traceability graph, tracing two of the model’s three named requirements from functional intent through allocation and realization to verification evidence, finds that deliveredEnergyBoundedBySupply is tied to no requirement usage at all, and closes that gap directly with EnergyConservationReq/energyConservationReq -- tied by subsetting the lemma from within the requirement’s own body, deliberately with no assert satisfy line, confirmed by a negative control that shows that idiom fails under model.verify_satisfaction() -- then records how that tie should honestly be read in a new judgment record, AC-C10; notebook 02 reconstructs three real ReviewRecords (AS-C06, AS-C08, AI-C06) into a ledger and reads what each one’s own kind, disposition and residual uncertainty actually says; notebook 03 synthesizes both into one new record, AI-C10, and states plainly that the record itself is not sign-off.
What this establishes¶
The traceability graph traces the model’s two requirements very differently, and says so honestly. heatGenerationReq has real, bidirectional verification evidence: rated really satisfies it, weak really fails it, both real claims about real candidates. timely traces just as far through a real functional intent, a real allocation and real physical candidates, but stops one link short of any positive verification at all: the only claim against it is negative (slow fails it), and Toaster::cycleTime is still not derived from anything, so no one has ever actually checked whether nominal satisfies it. And this tutorial’s own strongest piece of formal evidence, deliveredEnergyBoundedBySupply, proved by Z3 for every value its unbound features admit, was tied to no requirement usage anywhere in the model: 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 with no requirement in front of it. This chapter closes that gap rather than leaving it stated: EnergyConservationReq/energyConservationReq restates exactly the property the lemma proves 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 directly from within the requirement’s own body, confirmed by requirement_ties() before and after. Deliberately absent is an assert satisfy line: a direct test (the negative control in notebook 01) 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 -- requirement_coverage()'s own covered=False for energyConservationReq is therefore correct and expected, a different, by-design kind of “uncovered” from timely’s own real gap, not a second instance of it.
Closing a traceability gap is not the same as the closing requirement being independently motivated, and AC-C10 discloses this honestly rather than papering over it: the subsetting mechanism is spec-legitimate and the requirement’s own general motivation, energy conservation, is a genuine physical law, but its own need was identified retroactively, after Chapter 8’s proof already existed, specifically to close the gap this chapter’s own traceability analysis found -- a real, honestly-named assurance deficit, not a defect hidden behind a doc comment. AC-C10 also names a second, related limit: the tie rests on structural detection alone (Check B’s own subsetting hit), with no independent solver-level re-verification -- sysmlv2 verify --solve generates no separate check at all for a bare subsetting reference, confirmed directly in notebook 01.
The judgment ledger, built from three real records rather than asserted about all of them, shows what that graph’s own evidence is actually worth. AS-C06 stays undetermined: its own residual admits the mechanism selection could be revisited against a real trade study, not settled by the domain premise it currently rests on. AS-C08 is supported, but narrowly: its own residual is explicit that the proof is of a hand-restated companion lemma, not automatically re-checked against the real elements it mirrors if either is edited. AI-C06 stays undetermined too: its own residual leaves the branch’s further decomposition, composition into a real Toaster candidate, and ApplyHeat’s other flows all genuinely open. Two records out of three stay undetermined, and the one supported record is supported only for a claim already narrowed to a restated copy, not the real elements it mirrors.
The synthesis record, AI-C10, brings both together honestly, within its own stated scope: it names what has real, bidirectional evidence, what has only one-sided evidence, and how the model’s own strongest formal proof, once tied to no stated requirement at all, is now tied to the one requirement this chapter added to close that gap, with engineering_conclusion="undetermined", the only honest word for a model with one covered requirement, one uncovered one, and closing that one traceability gap settling neither. And it states, in its own prose, the distinction the whole chapter rests on: a completed traceability graph and judgment ledger are not sign-off itself. Sign-off is a human, accountable act; this tutorial can show the inputs to that act, honestly and within its own stated scope, but it does not, and should not, perform it on the learner’s behalf.
What comes next¶
This is the tutorial’s last chapter. What continues from here is not another chapter but the reader’s own accountable engineering: taking the traceable, honestly-scoped case this tutorial teaches how to build, and exercising, on a real design, the judgment this tutorial has shown but never made for them. If you come back to this repository, the contribution it wants is keeping it current to its toolchain and to the SysML v2 specifications, not extending it; the contributor guide says what that means.
Exercise¶
See exercises/ch10/exercise.ipynb: it asks you to build this same traceability graph, judgment ledger and sign-off synthesis over your own coffee-maker model.