Hello and welcome back to the Advent of SysML v2 – a daily, hands-on mini-course designed to bring you up to speed with the new SysML v2 standard and the modern Syside tooling that makes you productive from day one.

By the end of this lesson, you will:

• Learn how to model that an element shall satisfy a requirement
• Learn how to automatically verify requirements with Syside Automator

If you want to dive deeper into the world of SysML v2, check out The SysML v2 Book, where this topic is also discussed in more detail.

Requirement Satisfaction

In the previous lessons, we saw many useful patterns to define requirements. This time, we will focus on how to assert in the model that an element satisfies a requirement before actually verifying it with Automator.

As we mentioned yesterday, despite the name, a requirement is just a condition. If we want to assert that it is indeed satisfied by some component (or behavior, for that matter), we have to explicitly model that with satisfy requirement usages. A satisfy requirement usage is a requirement usage (like subrequirements are), but it also binds the subject of the requirement to its parent and asserts that it must evaluate to true in legal implementations of this model.

Let us recall the model from the previous lesson. We had a design for Santa’s sleigh that prescribed a cockpit and a cargo bay. We also had a requirement “DeliverGifts” that we decomposed into two subrequirements: one about the cockpit and one about the cargo bay. What is left to model is how these requirements are (or shall be) satisfied by our design.

Line 12 demonstrates a simple case. It models a satisfy requirement usage “satisfiedReq1” that is defined by the “DeliverGifts” requirement definition. This means that every instance of Santa’s sleigh will have a requirement instance of “DeliverGifts” such that the subject is this particular sleigh instance, and any and all the constraints prescribed by the “DeliverGifts” (including subrequirements) must evaluate to True. With one line, we prescribed that all the requirements grouped by “DeliverGifts” must be met by every sleigh built from this design.

Satisfy requirement usages usually do not need a name. This is illustrated in lines 20 and 27. These satisfy requirement usages also demonstrate the benefits of using requirement definitions even if they are grouped by other requirements: independently of the sleigh, we can specify that a specific cargo bay variant meets the requirements about cargo bays.

Recall the model from Lesson 8, where we defined two variants for the cargo bay: a magical one with ordinary bags, and an ordinary one with a bottomless bag. They are here again in lines 15–41, and now we can model that they both satisfy the requirement captured in “CargoCapacity”: they can both hold an arbitrary number of gifts.

Since this is not immediately apparent, we added “doc” comments in the body of the satisfy requirement usages to explain why each variant satisfies the requirements. The body could be used to specify values for any requirement parameters as well, although we recommend “closing” all parameterized requirements with concrete values in a specialization. This way, only the subject remains open, which is automatically bound by the satisfy requirement usage, and all the concrete requirements appear in one place (rather than being scattered in usages throughout the design).

Automated Verification with Automator

Having satisfy requirement in your model is a claim — you’re asserting that a component meets certain requirements. But how do you know that claim is actually true? This is where the formal constraints from Lesson 23 pay off.

Why Automated Verification Matters

In traditional workflows, verifying requirements is a manual process. An engineer reads the requirement text, looks at the design values, and makes a judgment: “Yes, this looks like it satisfies the requirement.” This works for simple cases, but it doesn’t scale. With hundreds of requirements across multiple subsystems, manual verification becomes error-prone and time-consuming. Worse, when design values change during iteration, you need to re-verify everything affected.

Automated verification changes this fundamentally. Because we expressed our requirements with mathematical constraints (not just prose), the computer can evaluate them. True or false, with no interpretation or judgment calls. And it can do this instantly, every time the model changes.

The Verification Process

Using Syside Automator, we can write a verification script that walks through the model and evaluates every requirement. The process is straightforward:

1. Find all satisfy requirement usages in a component
2. For each requirement, retrieve the subject and evaluate the constraints
3. Check assume constraints first (if they fail, the requirement doesn’t apply)
4. Evaluate require constraints to determine pass or fail
5. Recursively verify all subrequirements

The key insight is that this follows the requirement hierarchy you already defined. If you decomposed “DeliverGifts” into “CockpitForSanta” and “CargoCapacity,” the verification will check each subrequirement and roll up the results. A parent requirement passes only if all its children pass.

Here’s a simplified view of the core logic:

When we run this verification script on our Santa’s sleigh model, we get the following output:

Let’s look at the output. We can trace from SantaSleigh through DeliverGifts all the way down to CockpitSize. That’s requirements traceability, built into your model and automatically verified. Each ✅ confirms that the formal constraint evaluates to true for the actual design values.

When Verification Fails

What happens if a requirement isn’t satisfied? Let’s say someone reduces the cockpit volume from 500 liters to 300 liters. The verification script would produce:

The failure propagates up the hierarchy. CockpitSize fails, which causes CockpitForSanta to fail, which causes DeliverGifts to fail. The engineer immediately knows exactly which requirement failed and can trace it back to the specific constraint. No more guessing or hunting through spreadsheets.

Use Cases for Automated Verification

This verification capability enables several powerful workflows:

• Design Reviews: Before a milestone review, run verification on the entire model. Generate a report showing all requirements and their pass/fail status. Reviewers can focus their attention on failures rather than manually checking everything.
• Continuous Integration: As we saw in Lesson 20, you can integrate verification into your CI/CD pipeline. Every commit triggers automatic verification. If any requirement fails, the pipeline stops and notifies the team. Issues are caught immediately, not weeks later during integration.
• Trade Studies: When evaluating design alternatives, run verification on each variant. Which configurations satisfy all requirements? Which ones fail, and where? Automated verification turns trade studies from guesswork into data-driven decisions.
• What-If Analysis: “What if we reduce the cockpit size to save weight? What if Santa gains 10 kg over the holidays?” Change the values, run verification, and instantly see the impact on requirement compliance.
• Regression Testing: As the model evolves, requirements can be inadvertently violated by changes in seemingly unrelated areas. Running verification after every change catches these regressions immediately.

The key benefit is speed and consistency. Manual verification might happen once before a major review. Automated verification can happen hundreds of times a day, on every change, with perfect consistency.

The Final Challenge

This is what we teased in Lesson 23: formal constraints become automatically checkable. And as we saw in Lesson 20, you could integrate this verification into a CI/CD pipeline – every commit, every change, automatically verified against your requirements.

Your challenge is to practice requirement satisfaction and verification. Head over to Syside Cloud and do the following tasks, extending the example model from the lesson.

1. Add a satisfy requirement usage to connect your stealth mode requirements (from the Lesson 22 challenge) to the appropriate subsystems.
2. Run the verification script to confirm that all requirements pass.
3. Try changing a design value (e.g., reduce the cockpit volume) to see what happens when a requirement fails.

Summary

In this episode, you learned how to close the loop on requirements in SysML v2. You saw how satisfy requirement usages connect your design elements to the requirements they fulfill, and how Syside Automator can automatically verify those claims by evaluating the formal constraints you defined. Failures propagate up the requirement hierarchy, giving you immediate visibility into exactly what’s broken and why. Combined with CI/CD integration, this turns requirements from static documentation into continuously verified specifications. It is now time to try it at Syside Cloud by doing the challenge.

Thank you for being part of this 24-day journey. We hope the Advent of SysML v2 has given you a solid foundation to start modeling real systems with confidence. The language has even more to offer, and we’re excited to see what you’ll build with it. Happy modelling!