This notebook introduces verification def; after running it you can declare a named verification case that specifies how a requirement will be checked.
Notebooks 01–03 of this chapter established the requirement usage timely : TimelyToast, a satisfaction claim demonstrating the requirement’s failing branch (slow), and a threshold judgment record. A complete requirement has three parts (Part 4): description, rationale, and verification method. The first two are in TimelyToast’s doc comment (Chapter 2, §7.21.2). verification def in SysML v2 (§7.24) closes the anatomy by declaring how the requirement will be verified: the subject under test, and an objective that names the requirement usage to verify.
from pathlib import Path
import opensysml
from toaster.report import format_diagnostics
conn = opensysml.connect(version="v0.9.0")
# editor.add_verification_def(owner='ToasterDemo', name='TimelyToastTest', doc=..., subject_type='Toaster') when API ships
# spec: SysML v2 formal/2026-03-02 §7.24.2 (VerificationCaseDefinition)
VERIF_DEF_OPEN = "verification def TimelyToastTest {"
print(VERIF_DEF_OPEN)verification def TimelyToastTest {
verification def TimelyToastTest declares a reusable verification case for the toasting cycle requirement. Like requirement def, a verification def takes a subject (the system under test) and a body specifying what must be determined.
# editor.set_doc(owner='ToasterDemo::TimelyToastTest', text=...) when API ships
# spec: SysML v2 formal/2026-03-02 §7.21.2 (informal text applies to all elements including verification defs)
# Note: #verificationMethod = VerificationMethodKind::test metadata not yet supported (https://github.com/Open-MBEE/toaster/issues/19 / https://github.com/Open-MBEE/OpenSysML/issues/608)
# spec: SysML v2 formal/2026-03-02 §7.24 Table 22 (Verification Methods Compartment)
DOC_COMMENT = """\
doc /*
* Verification method: timed test of three consecutive toasting cycles at
* nominal input power; all must complete within 180 seconds.
* Method type: test (VerificationMethodKind::test, SysML v2 §7.24 Table 22).
* Note: formal #verificationMethod metadata not yet supported in OpenSysML v0.9.0;
* tracked at toaster#19 / OpenSysML#608.
*/"""
print(DOC_COMMENT) doc /*
* Verification method: timed test of three consecutive toasting cycles at
* nominal input power; all must complete within 180 seconds.
* Method type: test (VerificationMethodKind::test, SysML v2 §7.24 Table 22).
* Note: formal #verificationMethod metadata not yet supported in OpenSysML v0.9.0;
* tracked at toaster#19 / OpenSysML#608.
*/
The doc block holds the informal text of the verification case. It describes the verification method as a timed test. The formal #verificationMethod = VerificationMethodKind::test metadata annotation (§7.24 Table 22) is the spec-defined way to declare the method kind; it is not yet supported in the OpenSysML runtime v0.9.0 (toaster#19 / OpenSysML#608).
# editor.set_subject(owner='ToasterDemo::TimelyToastTest', subject_type='Toaster') when API ships
SUBJECT_DECL = " subject toaster : Toaster;"
print(SUBJECT_DECL) subject toaster : Toaster;
The subject toaster : Toaster declaration names the entity under test: any Toaster instance placed in this verification role.
# editor.set_objective(owner='ToasterDemo::TimelyToastTest', verify=['timely']) when API ships
# spec: SysML v2 formal/2026-03-02 §7.24.2: objective declares what requirements are verified
OBJECTIVE_BODY = """ objective {
verify timely;
}"""
print(OBJECTIVE_BODY) objective {
verify timely;
}
The objective block names the requirement usage being verified: timely : TimelyToast from notebook 01. verify timely is a shorthand satisfy constraint (§7.24.2) that asserts the objective is met when timely is determined to hold for the subject. verify takes a requirement usage, not a definition: verify TimelyToast would fail because TimelyToast is a requirementDef, not a usage.
TOASTER_INCREMENT = f"{VERIF_DEF_OPEN}\n{DOC_COMMENT}\n{SUBJECT_DECL}\n{OBJECTIVE_BODY}\n}}"
source = Path("../../models/ch03-cumulative.sysml").read_text()
model = conn.load_from_content(source, strict=False)
assert model.ok, f"Model failed: {format_diagnostics(model.diagnostics)}"The verification case loads without diagnostics. The next cell checks what happens when its objective names a requirement definition instead of a usage.
# Negative control: verify referencing a requirement def (not a usage) raises a type error.
bad_source = """
package Bad {
private import ScalarValues::*;
part def Toaster { attribute cycleTime : Real default = 120.0; }
requirement def TimelyToast {
subject toaster : Toaster;
require constraint { toaster.cycleTime <= 180.0 }
}
verification def BadCheck {
subject toaster : Toaster;
objective {
verify TimelyToast; // error: must be a requirement usage, not a def
}
}
}
"""
bad = conn.load_from_content(bad_source, strict=False)
assert not bad.ok, "Expected parse/semantic error for verify-on-def"
print("Expected error:", bad.diagnostics[0].message)Expected error: satisfy target must be a requirement usage, found requirementDef
With the negative control confirmed, the next cell looks up the verification case in the loaded model.
vd = model.find("ToasterDemo::TimelyToastTest")
assert vd is not None
print(f"verification kind : {vd.kind}")
print(f"verification id : {vd.id}")
for e in model.query():
d = e.as_dict()
if d["@type"] == "VerificationCaseDefinition":
print(f"VerificationCaseDefinition: {d['qualifiedName']}")
conn.close()verification kind : verificationCaseDef
verification id : ToasterDemo::TimelyToastTest
VerificationCaseDefinition: ToasterDemo::TimelyToastTest
The TimelyToastTest fragments printed above loaded without error, and model.find() returns its symbol, confirmed as a VerificationCaseDefinition by model.query() above.
Try the chapter exercise in exercises/ch03/exercise.ipynb: declare a BrewTempTest verification case for your coffee maker’s temperature requirement, with an objective that verifies the requirement usage from notebook 01.