Advent of SysML v2 | Lesson 23 – Formal Requirements, Constraints and Templates

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 about formally specifying requirements
  • Learn to use requirement templates

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.

Formal Requirements

Besides the powerful specialization and decomposition patterns presented in the previous lesson, SysML v2 also allows for the formal specification of requirements using actual logical constraints. Constraints are Boolean expressions that may have parameters. The benefit of this is that such formalized requirements can be evaluated automatically, potentially in a CI/CD pipeline, as you saw in Lesson 20. We will continue with the example model from Lesson 22, the next relevant excerpt of which is shown below.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
// …
package SantaSleighDesign {
    part def SantaSleigh specializes SantaSleighSpecification::SantaSleigh {
        part cockpit {
            attribute volume :> ISQ::volume = 500 [SI::L];
        }
        // …
        ref part santa {
            attribute weight :> ISQ::mass = 150 [SI::kg];
        }
        // …
    }
    // …
}

package RequirementBreakdown {
    private import SantaSleighDesign::*;
    // …
    requirement def <‘TR1.1> CockpitForSanta {
        subject sleigh : SantaSleigh;
        require constraint {
            language “English” /* The sleigh must have a cockpit for Santa. */
        }

        requirement : CockpitSize;
    }

    requirement def <‘TR1.1.1> CockpitSize {
        subject sleigh : SantaSleigh;
        doc /* The volume of the cockpit must be at least 3 times as much
             * as the volume of Santa. */
        assume constraint {
            sleigh.santa.weight >= 0
        }
        require constraint {
            sleigh.cockpit.volume >= 3 * sleigh.santa.weight / 1.03 [SI::kg/SI::L]
        }
    }
    // …
}

Let us first focus on the definition of “CockpitForSanta” in line 19. We have been using the “doc” comment for the requirement text so far, but here is a more precise way that moves towards formal requirements. In line 21, we declare a require constraint. It represents the constraint that must be true over the requirement parameters in order to satisfy the requirement. We still want to use an English sentence to describe the constraint, but we now have a model element to actually represent it, so it makes sense to use a textual representation (introduced in Lesson 10) inside it. Similarly, we could use another programming or modeling language.

The next step is to actually model the constraint in SysML. Our goal is to model a subrequirement of “CockpitForSanta” that specifies the minimum cockpit size. For the sake of simplicity, we will measure the volume of the cockpit rather than its dimensions. Since Santa’s sleigh is a customized sleigh for Santa, we want to base this requirement on Santa’s parameters. Line 9 models Santa’s weight, which we will use to estimate his volume. We also have an attribute to record the size of the cockpit, as shown in line 5.

With that in mind, let us define the “CockpitSize” requirement in line 28. We use the sleigh as a subject and document the requirement in English. Then, we define the constraint formally in line 35. The expression specifies that the volume of the sleigh’s cockpit is at least three times as much as Santa’s weight converted to volume, assuming Santa weighs 1.03 kilograms per liter of volume. When we learn or decide these values in the later phases of the design process, we can substitute them into the expression and see if it evaluates to true or false.

You can also see another kind of constraint in line 32. This is an assume constraint that records the assumptions that must be true for the requirement to make sense. If an assume constraint evaluates to false, the requirement is not considered violated even if the require constraint also evaluates to false. This can be useful if we want to limit requirements to different operational domains, as if they were “guarded”. We can define several requirements that capture the constraint for a given interval of parameters, and only the one that covers the actual values will have to be true when we evaluate the parent requirement. This example is slightly more boring: we just assume that Santa’s weight is positive.

With formal requirements, tools can help us identify contradictions or automatically evaluate the requirements against our designs. We will see how Syside supports this in the next lesson.

Requirement Templates

Formally specified requirements open up the possibility of modeling requirement templates that can be reused with different parameters. Let us generalize the “CockpitSize” requirement into a template about the ratio of different values.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
// …
package RequirementTemplates {
    requirement def SizingRequirement {
        doc /* The value of {toSize} must be at least {minimumScale} times
             * as large as {toFit}. */
        attribute toSize;
        attribute toFit;
        attribute minimumScale;
        assume constraint {
            toFit >= 0
        }
        require constraint {
            toSize >= toFit * minimumScale
        }
    }
}

package RequirementBreakdown {
    private import SantaSleighDesign::*;
    private import RequirementTemplates::*;
    // …
    requirement def <‘TR1.1.1> CockpitSize specializes SizingRequirement {
        subject sleigh : SantaSleigh;
        doc /* The volume of the cockpit must be at least 3 times as much
             * as the volume of Santa. */
        attribute :>> toSize = sleigh.cockpit.volume;
        attribute :>> toFit = sleigh.santa.weight / 1.03 [SI::kg/SI::L];
        attribute :>> minimumScale = 3;
        // constraint is inherited from specialized requirement
    }
    // …
}

We will declare the template in a different package. Line 3 shows that a template is just a very generic requirement definition. We do not even specify the subject, but we specify three additional attributes that serve as parameters of the template: “toSize” will be the value to be at least as large as “toFit” times the “minimumScale”. The constraint is captured in line 10.

Using this template, we can remodel the “CockpitSize” requirement. Since the template already captures the key constraint, we only need to specify he values for its attributes. We keep the subject definition, and redefine all three attributes: “toSize” will be the volume of the sleigh’s cockpit, “toFit” will be Santa’s volume estimated from his weight, and the “minimumScale” is 3. We do not need to redeclare the constraint because it is inherited from the template, and already uses the attributes we have just redefined.

With this pattern, we can generalize a family of requirements and reuse the templates for different components or variants.

Challenge for Tomorrow

Your challenge is to practice the formal modeling of requirements. Head over to Syside Cloud and do the following tasks, extending the example model from the lesson, potentially building on your solution from yesterday.

  1. Take the requirement about stealth mode from yesterday. Use the sample solution if you have not solved the challenge yesterday.
  2. Introduce a formal subrequirement into the “SufficientPower” requirement definition that requires the capacity (in kWh) of the power subsystem to be greater than the power requirement (in W) of the stealth subsystem times the mission time, which is 24 hours.
    1. Introduce the necessary features into the subsystems.
  3. Refactor the requirement to use the “SizingRequirement” template from the lesson.

Summary

In this episode, you learned about formal requirements in SysML v2, which allows for a lot more precision and even automatic evaluation. You saw how this, coupled with specializations, enables requirement templates, a powerful way to reuse requirements in different designs. It is now time to try it at Syside Cloud by doing the challenge. Don’t forget to come back tomorrow for another episode of the Advent of SysML v2!

Cookies

Learn SysML v2 through the Advent of SysML v2 Challenge!