Requirements and Verification

Your coffee machine has structure, connections, behavior, states, and constraints. You can describe what the system is made of, how it behaves, and what rules it must obey. But none of that answers a fundamental engineering question: does the design actually meet what was asked for?

That is what requirements and verification are for. A requirement captures something the system must do or be. A satisfaction link says which part of the design addresses it. A verification case says how you plan to prove it. Together, these three elements form a traceability loop – the mechanism that connects stakeholder intent to design decisions to objective evidence.

SysML v2 models requirements as first-class elements, not as external documents referenced by ID. They live in the same model as the parts, actions, and constraints they trace to. This means tools can check whether every requirement has a design link and a verification plan, rather than relying on spreadsheets and manual audits.

Defining a Requirement

A requirement starts with requirement def. Like part definitions and action definitions, a requirement definition is a reusable type. You can give it a short identifier (useful for document references) and a doc comment that carries the requirement text.

The short identifier goes in angle brackets and single quotes – <'REQ-TEMP-001'>. The quotes are what let it contain hyphens, which a plain identifier cannot; Appendix H covers that form and the rest of the naming rules.

package CoffeeMachineRequirements {
    requirement def <'REQ-TEMP-001'> BrewTempReq {
        doc /* The brewer extraction temperature shall remain
               between 90 and 96 degrees Celsius during brewing. */
    }
}

BrewTempReq is the model name you use in SysML code. REQ-TEMP-001 is the short ID – a human-readable tag that maps to whatever requirement numbering scheme your project uses. The doc comment holds the requirement text itself. This text is not checked by the model, but it is visible to reviewers and tools.

You can define as many requirements as your project needs. Here is a second one for the safety interlock from Chapter 9:

package CoffeeMachineRequirements {
    requirement def <'REQ-TEMP-001'> BrewTempReq {
        doc /* The brewer extraction temperature shall remain
               between 90 and 96 degrees Celsius during brewing. */
    }

    requirement def <'REQ-SAFE-001'> SafetyInterlockReq {
        doc /* The system shall not initiate a brew cycle
               unless a cup is detected on the drip tray. */
    }
}

Each requirement stands alone as a definition. It does not yet say anything about which part of the design addresses it or how you would test it. Those connections come next.

Requirement Text vs. Formal Constraints

The doc comment on a requirement is prose. It communicates intent to human readers, but the model checker cannot evaluate it. For requirements where precision matters, you can add a formal constraint inside the requirement body.

requirement def <'REQ-TEMP-001'> BrewTempReq {
    doc /* The brewer extraction temperature shall remain
           between 90 and 96 degrees Celsius during brewing. */

    attribute temp : Real;
    require constraint { temp >= 90.0 and temp <= 96.0; }
}

The require constraint block adds a machine-checkable condition alongside the prose. The temp attribute is a parameter of the requirement – it represents whatever value needs to satisfy the condition. When this requirement is linked to a design element, the attribute can be bound to an actual property.

A formal constraint also turns the requirement into something the runtime can produce evidence for. During constraint evaluation, verification, or simulation-coupled verification, the constraint runs against the bound values and produces a Pass / Fail / Inconclusive / Error verdict (covered in How Verification Verdicts Work, below).

Not every requirement needs a formal constraint. Some requirements are inherently qualitative (“the user manual shall be written in English”) and do not benefit from formalization. The general rule: if the requirement text contains a number, a range, or a logical condition, consider adding a require constraint to make it checkable.

Subjects, Actors, and the Binding Surface

A requirement can declare a subject – the element it constrains. The subject says “this requirement is about that thing.”

requirement def <'REQ-TEMP-001'> BrewTempReq {
    doc /* The brewer extraction temperature shall remain
           between 90 and 96 degrees Celsius during brewing. */

    subject brewer : Brewer;
}

The subject keyword declares that BrewTempReq applies to a Brewer. This is a typed parameter: any element that satisfies this requirement must be (or contain) a Brewer. Subjects make requirements more precise. Without a subject, a requirement floats – you know it exists, but not what it applies to. With a subject, the requirement is anchored to a specific kind of element.

A requirement can also declare one or more actors – the elements that interact with the subject. Actors are typed in the same way as subjects:

requirement def <'REQ-SAFE-001'> SafetyInterlockReq {
    doc /* The system shall not initiate a brew cycle
           unless a cup is detected on the drip tray. */

    subject machine : CoffeeMachine;
    actor user : Operator;
}

The actor declaration says “this requirement is about how the Operator interacts with the CoffeeMachine.” Actors are useful when a requirement is fundamentally about an interaction, not just a property of a single part.

Together, the subject, the actors, and any attribute parameters form the requirement’s binding surface – the set of names that a satisfy site must supply. The binding surface is also the scope inside which a require constraint resolves names (recall Chapter 9, “How Constraints Find Their Values”). When the runtime evaluates the constraint, it walks this surface, not the surrounding package, to find values.

Why this matters. Authors often write require constraint bodies that reference attributes the requirement does not declare. The constraint then either picks up the wrong attribute by accident or fails to evaluate because no value is bound. The fix is to declare every name the constraint uses as part of the binding surface – subject, actor, or attribute – so the satisfy site has a clean place to supply them.

Satisfying a Requirement

A requirement on its own is just an assertion about what should be true. To close the loop, you need to say which part of the design addresses it. That is what satisfy does.

part def CoffeeMachine {
    part brewer : Brewer;

    satisfy requirement : BrewTempReq;
}

The satisfy statement inside CoffeeMachine says: this design element claims to address BrewTempReq. The exact strength of that claim depends on the requirement.

Requirements with no formal constraint are pure traceability links. The model does not check whether CoffeeMachine actually meets the qualitative goal – the link just makes the relationship explicit and queryable. A tool or a reviewer can ask “which requirements does CoffeeMachine satisfy?” and get a definitive answer.

Requirements that carry a require constraint are stronger. The satisfy site supplies the bindings for the requirement’s parameters (subject, actors, attributes), and at evaluation time – whether driven by a static check, a verification case, or a simulation – the constraint is evaluated against those bindings and produces a verdict. This is not a manual claim; the model knows whether the constraint holds for the values the satisfy site supplied. We unpack the verdict shape in How Verification Verdicts Work, below.

You can satisfy multiple requirements from the same design element:

part def CoffeeMachine {
    part brewer : Brewer;
    part grinder : Grinder;
    part waterTank : WaterTank;

    satisfy requirement : BrewTempReq;
    satisfy requirement : SafetyInterlockReq;
}

You can also place satisfaction links at a more specific level. If the temperature requirement is really about the brewer, not the whole machine, put the satisfaction there:

part def Brewer {
    attribute waterTemp : Real;
    attribute brewPressure : Real;

    satisfy requirement : BrewTempReq;
}

Where you place the satisfy link is a modeling decision. Put it at the level of the design element that is actually responsible for meeting the requirement. If the brewer controls the temperature, the brewer should carry the satisfaction link.

Verification Cases

Satisfaction says “this design addresses this requirement.” But that is a claim, not evidence. Verification cases capture how you plan to produce evidence.

A verification case is defined with verification def. Inside it, an objective block declares which requirement it verifies:

verification def BrewTempTest {
    doc /* Measure extraction temperature across 10 consecutive
           brew cycles and confirm all readings fall within range. */

    objective {
        verify requirement : BrewTempReq;
    }
}

BrewTempTest is a verification case that targets BrewTempReq. The doc comment describes the test procedure in prose. The verify statement inside the objective block creates the formal link.

A verification case can verify more than one requirement:

verification def SafetyInterlockTest {
    doc /* Attempt to start a brew cycle with no cup present.
           Confirm the system rejects the command. Then place a cup,
           retry, and confirm the cycle starts. */

    objective {
        verify requirement : SafetyInterlockReq;
    }
}

You can also define actions inside a verification case to describe the test procedure as modeled steps:

verification def SafetyInterlockTest {
    doc /* Verify that the brew interlock prevents operation
           without a cup. */

    action removeCup { doc /* Remove any cup from the tray. */ }
    action attemptBrew { doc /* Press the brew button. */ }
    action confirmRejection { doc /* Verify the machine refuses to brew. */ }
    action placeCup { doc /* Place a cup on the tray. */ }
    action retryBrew { doc /* Press the brew button again. */ }
    action confirmSuccess { doc /* Verify the brew cycle starts. */ }

    first removeCup then attemptBrew then confirmRejection
        then placeCup then retryBrew then confirmSuccess;

    objective {
        verify requirement : SafetyInterlockReq;
    }
}

This level of detail is optional. For many projects the prose description in doc is sufficient. But when your verification plan will eventually drive automated test execution or when reviewers need to see the exact sequence, modeling the steps as actions makes the procedure unambiguous. The essential thing is the verify link – it connects the requirement to a planned piece of evidence.

How Verification Verdicts Work

sysml-rs extends the spec here. The OMG spec defines verify as a relationship that produces an outcome, but does not normatively define the outcome’s shape. sysml-rs settles on a four-valued verdict with a structured payload, described below. Other SysML v2 implementations may produce different verdict shapes; the spec-level traceability still works either way.

When a requirement that carries a require constraint is evaluated – by a verify case, by assert constraint running against the satisfy site, or by a simulation step – the result is a verdict. A verdict is one of four values:

• Pass — the constraint evaluated to true against the bound values. The requirement is met for this evaluation.
• Fail — the constraint evaluated to false. The requirement is violated.
• Inconclusive — the constraint did not have enough information to decide (for example, an attribute on the binding surface had no assigned value, or the evaluation depended on a not-yet-simulated time point).
• Error — the evaluation itself broke (a name did not resolve, a type mismatch, division by zero). The model has a defect that must be fixed before the verdict means anything.

A verdict carries more than just the kind. The structure typically looks like this:

Verdict {
    kind:      Pass | Fail | Inconclusive | Error
    actual:    <value the constraint evaluated to>
    expected:  <value the constraint required>
    margin:    <how close to the boundary, when applicable>
    message:   <human-readable explanation>
    evidence:  <reference to the source: a tick number, a test step, etc.>
}

For BrewTempReq with the constraint temp >= 90.0 and temp <= 96.0, three sample verdicts might look like:

Pass:          actual=92.4, expected=[90.0, 96.0], margin=2.4
Fail:          actual=98.1, expected=[90.0, 96.0], margin=-2.1
Inconclusive:  actual=null, message="`temp` had no assigned value"
Error:         message="undefined variable: `specification.temperature`"

The Inconclusive case is the one that surprises authors. A passing verdict is good news; a failing verdict tells you something concrete to fix; an Error is a model bug; but Inconclusive says the model is incomplete – the constraint is well-formed and the design site is willing to be checked, there just is not yet a value to check against. In a static review, that means the satisfy site needs to bind a missing parameter. In a simulation, it usually means the constraint is being checked before the relevant state variable has been initialised.

Treat each kind as actionable:

• Pass → record evidence; you have met the requirement.
• Fail → fix the design or relax the requirement (with stakeholder agreement).
• Inconclusive → bind the missing values; complete the model.
• Error → fix the model; the constraint is unevaluable as-written.

Verifying Against a Simulation

sysml-rs extends the spec here. Coupling a verify to a running simulation – so the verdict is computed from time-series state, not from static attribute values – is one of sysml-rs’s intended use cases. The OMG spec is more abstract about how verification produces its outcome.

For requirements that constrain behaviour over time (a temperature stays in range, a cycle completes within a deadline), the natural evidence is a simulation run. Here is what that looks like end-to-end for the coffee machine.

In Chapter 9 you saw the :> GetDerivative pattern for ODE right-hand sides. The brewer’s heater, modelled as a state with an ODE, looks like:

import StateSpaceRepresentation::*;

calc def HeaterRhs :> GetDerivative {
    in t : Real;
    in temp : Real;
    in heaterPower : Real;
    in lossCoeff : Real;
    in thermalMass : Real;
    return dT_dt : Real = (heaterPower - lossCoeff * temp) / thermalMass;
}

The brewer holds the state variable waterTemp and uses HeaterRhs to advance it. Now we tie verification to that:

package CoffeeMachineVerification {
    import CoffeeMachineDomain::*;
    import CoffeeMachineRequirements::*;

    verification def BrewTempSimulationTest {
        doc /* Simulate one brew cycle. The brewer's waterTemp must
               stay within [90.0, 96.0] across the entire extraction
               window. */

        subject brewer : Brewer;

        objective {
            verify requirement BrewTempReq {
                in temp = brewer.waterTemp;
            }
        }
    }
}

The verify requirement block binds the requirement’s temp parameter to the simulated brewer.waterTemp. When the verification runs against a simulation:

1. The simulation advances waterTemp over time using HeaterRhs.
2. At each tick, the require constraint is evaluated against the current waterTemp value.
3. If waterTemp ever leaves [90.0, 96.0], the verdict is Fail and the evidence carries the offending tick.
4. If waterTemp stays in range across the whole simulated window, the verdict is Pass.
5. If the simulation never starts heating (a stuck binding, a missing input), the verdict is Inconclusive for that window.

The shape that makes this work is the same shape as the rest of the chapter: a requirement with a typed binding surface, a require constraint body that resolves names against that surface, and a verify link that supplies the bindings – only this time the bindings come from running state, not from a static attribute.

Why this matters. A numerical requirement (a temperature, a duration, a tolerance) is rarely satisfiable by inspection. Coupling verify to a simulation gives you primary evidence: the constraint either held over the simulated trajectory or it did not, and you can replay the failing tick. The chapter’s earlier verification cases describe what you would do; this is what you can run.

The Full Traceability Loop

With requirements, satisfaction, and verification in place, you have a complete traceability loop. Here it is for the coffee machine, all in one package:

package CoffeeMachineRequirements {
    import ScalarValues::*;
    import CoffeeMachineDomain::*;

    // --- Requirements ---

    requirement def <'REQ-TEMP-001'> BrewTempReq {
        doc /* The brewer extraction temperature shall remain
               between 90 and 96 degrees Celsius during brewing. */

        subject brewer : Brewer;

        attribute temp : Real;
        require constraint { temp >= 90.0 and temp <= 96.0; }
    }

    requirement def <'REQ-SAFE-001'> SafetyInterlockReq {
        doc /* The system shall not initiate a brew cycle
               unless a cup is detected on the drip tray. */

        subject machine : CoffeeMachine;
    }

    requirement def <'REQ-BREW-001'> BrewTimeReq {
        doc /* A brew cycle shall complete within 60 seconds
               from initiation to coffee dispensed. */

        subject machine : CoffeeMachine;

        attribute duration : Real;
        require constraint { duration <= 60.0; }
    }

    // --- Satisfaction (in a usage context) ---

    part coffeeMachine : CoffeeMachine {
        satisfy requirement : BrewTempReq;
        satisfy requirement : SafetyInterlockReq;
        satisfy requirement : BrewTimeReq;
    }

    // The form above is the most common, but the spec also accepts:
    //
    //     satisfy requirement brewTempReq : BrewTempReq by brewer;
    //
    // which gives the satisfaction usage its own name (`brewTempReq`)
    // and lets you spell out which design element does the satisfying
    // (`by brewer`) when it is not the enclosing element.

    // --- Verification ---

    verification def BrewTempTest {
        doc /* Measure extraction temperature across 10 consecutive
               brew cycles. All readings must fall between 90 and
               96 degrees Celsius. */

        objective {
            verify requirement : BrewTempReq;
        }
    }

    verification def SafetyInterlockTest {
        doc /* Attempt brew with no cup: confirm rejection.
               Place cup, retry: confirm cycle starts. */

        objective {
            verify requirement : SafetyInterlockReq;
        }
    }

    verification def BrewTimeTest {
        doc /* Time 5 consecutive brew cycles from button press
               to coffee dispensed. All must complete within
               60 seconds. */

        objective {
            verify requirement : BrewTimeReq;
        }
    }
}

Read this from the bottom up: BrewTempTest verifies BrewTempReq, which is satisfied by coffeeMachine. That is one complete loop. Every requirement has a design link (who addresses it) and an evidence link (how you check it). A reviewer can trace from any requirement to both its design rationale and its verification plan.

This is where SysML v2 earns its keep as an engineering tool. The model is not just a picture of the system – it is a queryable database of commitments. You can ask:

• Which requirements have no satisfaction link? (Unaddressed requirements.)
• Which requirements have no verification case? (Unverified claims.)
• Which verification cases are not linked to any requirement? (Orphan tests.)

These are the questions that project reviews are built around. With model-based requirements, the answers come from the model itself rather than from manually maintained traceability matrices.

Requirement Decomposition

Large requirements are hard to verify directly. A common pattern is to decompose a top-level requirement into smaller, testable pieces. You can express this using nested requirements or by specializing a parent requirement.

requirement def <'REQ-PERF-001'> PerformanceReq {
    doc /* The coffee machine shall deliver acceptable
           performance across all operating conditions. */

    requirement <'REQ-PERF-001a'> startupTimeReq {
        doc /* The machine shall reach operating temperature
               within 90 seconds of power-on. */
    }

    requirement <'REQ-PERF-001b'> brewTimeReq {
        doc /* Each brew cycle shall complete within
               60 seconds of initiation. */
    }
}

The nested requirements startupTimeReq and brewTimeReq are children of PerformanceReq. Each child can have its own satisfaction and verification links. The parent captures the high-level intent; the children are the testable leaves.

Keep decomposition shallow. One or two levels is usually enough. Deep requirement hierarchies create more traceability overhead than they solve.

Use Cases and Concerns

SysML v2 includes two related concepts that provide context for requirements.

A use case describes a goal-oriented interaction with the system. It is defined with use case def:

use case def BrewEspresso {
    doc /* The user selects espresso, the machine grinds beans,
           heats water, extracts coffee, and dispenses into cup. */

    subject machine : CoffeeMachine;
    objective {
        doc /* Deliver a single espresso shot to the user. */
    }
}

Use cases sit at a higher level than actions. Where an action definition describes a sequence of steps, a use case describes a stakeholder goal. Use cases are useful for capturing “why does this behavior exist?” and for organizing requirements around user-facing scenarios.

A concern captures a stakeholder interest or worry:

concern def SafetyConcern {
    doc /* The machine must not create burn hazards or
           dispense onto the counter without a cup. */
}

Concerns are lightweight. They give requirements a “why” – a named reason for their existence. You do not need concerns for every requirement, but they help when a reviewer asks “why does this requirement exist?” and the answer involves stakeholder context that is not obvious from the requirement text alone.

Both use cases and concerns are optional. Many projects work fine with just requirements, satisfaction, and verification. Add use cases when you need to organize requirements around user goals. Add concerns when stakeholder rationale needs to be explicit.

Analysis Cases

A verification case asks a yes/no question – does the design meet the requirement? An analysis case asks a different question – what is the answer? – and returns a typed result. Use analysis def:

analysis def ThermalLossAnalysis {
    doc /* Estimate the heat lost from the brewer during a 30-second
           idle period at an ambient temperature of 20 degrees C. */

    subject brewer : Brewer;
    return lossRate : Real;
}

analysis def defines a case whose purpose is to compute something, not to check something. The body is shaped like the calc def from Chapter 9: it declares inputs (here, via the subject), does work, and returns typed outputs. The difference from a bare calc is that an analysis case carries the same envelope as a verification case – a subject, a doc-driven purpose, optional actor – so it sits inside the same traceability structure as the rest of the model.

Reach for analysis def when the engineering question is estimation (worst-case heat loss, peak load, mean time to brew) rather than compliance. The analysis case can even feed a verification case: it produces the number the verification case then checks against a requirement.

The General case Envelope

Verification, analysis, and use cases are siblings. All three are specializations of a single case def:

case def ThermalLoadProfile {
    subject brewer : Brewer;
    return idleLoad : Real;
    return heatingLoad : Real;
}

case def is the common envelope. Every case definition can carry a subject, an optional actor, an objective, and a body. verification def adds a verify requirement linkage; analysis def adds return values; use case def adds stakeholder actions. The grammar equips them with the same structure; the intent is what you choose when you pick the keyword.

For most modeling, you spell out the specific kind (verification def, analysis def, use case def) and never write the bare case def. But knowing they share an envelope pays off when you build tooling that treats all three uniformly, or when you specialize a case family of your own.

Rolling Up Verdicts Across Cases

The How Verification Verdicts Work section above defined a single verdict’s four values – Pass, Fail, Inconclusive, Error. A requirement is rarely checked once. It is checked against several verification cases, or, in a simulation-coupled verification, at every tick of a run. The individual verdicts are rolled up into one overall judgement for the requirement:

• If every verdict is Pass, the requirement is Pass.
• If any verdict is Fail, the requirement is Fail. A single failing observation is enough – the requirement was violated.
• If there are no Fail verdicts but at least one Inconclusive, the requirement is Inconclusive. You cannot claim Pass when part of the evidence was undecidable.
• If all verdicts are Error, the requirement is Error – the model itself is broken and no verification result is trustworthy until it is fixed.

This rollup is what makes verification metric-able. A project dashboard can report a pass rate per requirement (how many of its checks were Pass), flag requirements with outstanding Inconclusive verdicts, and surface the requirements carrying the most fails. The point of the four-valued verdict – and especially the Inconclusive case – is that absence of a fail is not the same as a pass. Rollup preserves that distinction at the requirement level.

Putting It Together: The Coffee Machine Grows

The coffee machine now has three layers of traceability. Here is how the pieces connect:

Structure (from Chapter 2 through Chapter 6): CoffeeMachine contains Grinder, Brewer, and WaterTank, connected through ports and interfaces.

Behavior (from Chapter 7 and Chapter 8): BrewCycle defines the action sequence. MachineStates defines the operating modes with guarded transitions.

Constraints (from Chapter 9): BrewTempSafe checks the temperature range. SafetyInterlock prevents brewing without a cup.

Requirements and verification (this chapter): BrewTempReq, SafetyInterlockReq, and BrewTimeReq capture the engineering intent. Satisfaction links connect them to the design. Verification cases connect them to evidence.

The constraints from Chapter 9 and the requirements from this chapter serve different purposes. A constraint is a rule the model enforces – it evaluates to true or false against actual values. A requirement is a commitment the project tracks – it may reference a constraint, but its primary purpose is traceability.

Consider the temperature range. In Chapter 9, you defined:

constraint def BrewTempSafe {
    in temp : Real;
    temp >= 90.0 and temp <= 96.0;
}

In this chapter, you defined:

requirement def <'REQ-TEMP-001'> BrewTempReq {
    doc /* The brewer extraction temperature shall remain
           between 90 and 96 degrees Celsius during brewing. */
    attribute temp : Real;
    require constraint { temp >= 90.0 and temp <= 96.0; }
}

These are not redundant. The constraint lives in the design and can be asserted against actual values during analysis or simulation. The requirement lives in the traceability structure and connects to satisfaction links, verification cases, and project reviews. You can have a constraint without a requirement (an internal design rule that nobody asked for) and a requirement without a constraint (a qualitative goal that cannot be formalized). When both exist for the same concern, the constraint makes the requirement checkable and the requirement makes the constraint traceable.

Visualizing Requirements and Traceability

Common Mistakes

Satisfaction without verification. A satisfy link is a claim, not evidence. If you satisfy a requirement but never define a verification case for it, you have an unverified claim. Some tools will flag this, but even without tooling, make it a habit: every satisfy should have a corresponding verify somewhere.

Requirements with no subject. A requirement without a subject can still be satisfied, but it is harder for reviewers to understand what it applies to. When you know which element a requirement targets, say so with subject.

Overly deep decomposition. Splitting one requirement into ten sub-requirements creates a maintenance burden. Each sub-requirement needs its own satisfaction and verification links. Prefer fewer, testable leaf requirements over deep hierarchies.

Duplicating constraint logic in requirements. If you already have a constraint def BrewTempSafe from Chapter 9, you do not need to rewrite that logic inside the requirement. You can reference the constraint or simply note in the requirement text that the constraint captures the formal condition. Do not maintain the same expression in two places.

What You Have Built

Your coffee machine model now includes:

• Three requirements with short IDs, prose text, subjects, and formal constraints
• Satisfaction links from the design to each requirement
• Verification cases with objectives that trace back to each requirement
• A complete traceability loop: requirement to design to evidence

This is the layer that makes the model auditable. In Chapter 11, you will assemble all of these pieces – structure, behavior, constraints, requirements, and verification – into one coherent system model.