Automated Reasoning for SysML v2 Part 2
Formally Verifying SysML v2 Constraints with Imandra
I previously published an article entitled “Automated Reasoning for SysML v2.” The article outlined how the Imandra Automated Reasoning enables complex reasoning about the design and formal verification of properties and behaviors. The example we shared in that article demonstrated formal verification of three verification goals for a traffic light designed using the pilot implementation of Systems Modeling Language version 2 (SysML v2.):
1. The behavior is deterministic, regardless of state or parameter values.
2. Errors are handled properly, irrespective of state or parameter values.
3. The light only switches to green when it is safe (all other lights in the system are red), irrespective of state or parameter values.
The article focused on the second verification goal, “Errors are handled properly.” Several systems engineers and developers working on SysML v2 read the article or reviewed my example and provided encouragement and positive feedback. They also had some great ideas of what I should do next. More than one person recommended that we synthesize verification goals directly from SysML v2 requirements and constraints. Again, I am excited to share my progress over the past couple of weeks.
Using Imandra Automated Reasoning with SysML v2
SysML v2 is a general-purpose modeling language for complex system design developed by the Object Management Group (OMG) as an open standard. The OMG released the beta implementation in July of 2023, and I expect the final release to be next summer. For more information on the SysML v2 release schedule, go to omg.org.
I am excited about SysML v2 for several reasons. After working with SysML v2 for the last few months, I have found it easy to learn. Unlike SysML v1, the language is consistent across all the modeling elements, such as parts, ports, connections, states, and so on. I am perhaps most excited about SysML v2’s formal semantics and the opportunities this creates. Formal semantics will ensure that there is a single representation of a SysML v2 model that contains all of its elements and relationships. The SysML v2 formal semantics will allow us to cleanly transpile SysML v2 models to the Imandra Modeling Language (IML). Once we have converted a SysML v2 design, we can formally verify the design against requirements, constraints and other verification goals. I am confident with the approach we are taking that system engineers can define verification goals natively in SysML v2 and still take advantage of Imandra’s automated reasoning tools without having to learn a second modeling language.
To demonstrate how Imandra can verify a system designed using SysML v2 we modeled a traffic light using SysML v2 and then converted it to IML. This manual conversion has helped create a guide and roadmap for the automatic SysML v2 to IML conversion tool (a “transpiler”). The SysML v2 traffic light model is based on the standard green, yellow and red traffic light used in the United States. We chose the traffic light because it is complicated enough to demonstrate some key capabilities of both SysML v2 and Imandra, while not being so complex that it would be difficult to understand. In the last article we focused on the behavior of the traffic light. This article will focus on two SysML v2 constraints. We will convert both constraints to formal verification goals in Imandra. Reviewing my first article, “Automated Reasoning for SysML v2,” may be useful before continuing.
Constraints and Verification Goals
SysML v2 models consist of elements and their relationships. One specific type of SysML v2 element is a constraint. A constraint has inputs and always returns a Boolean value. If the Boolean value returned is true, then the constraint is met, if it is false, then the constraint is not met. The input values to the constraint are not limited, except that they must be resolved through calculations and logic to a single Boolean result.
Formal requirements in SysML v2 are a special type of constraint, so for this article and example, you can think of constraints and requirements as interchangeable terms. The techniques and approaches we cover here will apply to both constraints and formal requirements.
Imandra Automated Reasoning has many capabilities, one of which is formal verification. With Imandra, we can mathematically prove the properties of a system using the Imandra verify function. The verify function leverages a variety of solvers and techniques behind the scenes to verify (or prove) that any function or expression is true. If Imandra is unable to prove that an expression or function is true for all parameters and states of the system, Imandra will provide a counterexample illustrating a case where the expression or function does not hold as true.
Constraints in SysML v2 map directly to Imandra verification goals. Both SysML v2 constraints and Imandra verification goals are very general and are defined as a function or expression that takes any number of parameters as inputs and returns a Boolean result. I am going to share two examples of SysML v2 constraints mapped to Imandra verification goals. One is trivial, and the second is significantly more complex.
Mapping Traffic Light Constraints to Verification Goals
In my prior article, we verified three behavioral properties of the traffic light:
1. The behavior is deterministic, regardless of state or parameter values.
2. Errors are handled properly, irrespective of state or parameter values.
3. The light only switches to green when it is safe (all other lights in the system are red), irrespective of state or parameter value.
In this article, we are going to verify weight and power usage against a limit. Verifying weight for a single system design without variation parts or parts that have fluctuating weight is a trivial task, and there are tools and examples in the SysML v2 language of how to create and resolve these types of constraints. Evaluating power consumption is significantly more complicated, automated reasoning is required to ensure that the power consumption requirement is met across all operational states and parameters.
Let us start with the weight constraint and verification goal. Below we have a SysML v2 constraint definition and constraint usage. The constraint definition for the traffic-light weight is as follows.
constraint def MassConstraint {
in partMasses : MassValue[0..*];
in massLimit : MassValue;
sum(partMasses) <= massLimit
}This constraint definition takes two inputs: a list of MassValues and a massLimit. The constraint definition returns a Boolean result based on a predicate defined as the sum of all the MassValues to be less than or equal to the massLimit. We then create an Assert Constraint usage based on this definition.
Assert constraint massConstraint : MassConstraint {
in partMasses =
(light_housing.totalMass,
tl_controller.mass,
tl_counter.mass,
tl_radio.mass);
in massLimit = 25.0 [kg];
}There are several other ways to define this list of masses. In the SysML v2 examples, there is a concept of a “mass rollup.” We used that approach here, and the whole system mass includes the “totalMass” for the light_housing that includes: the mass of the three lights (green, yellow, red), 3 inserts, the electronics housing, and light housing itself. The light_housing.totalMass plus the mass for the controller, counter, and radio give us the whole system mass tied to this constraint. The controller, counter, and radio are not in the light_housing>totalMass because they are not part of the light_housing part hierarchy. This example is an asserted constraint. In SysML v2 the difference between a constraint and an asserted constraint is that asserted constraints always must return true and often have a stakeholder (like the customer) tied to them.
Resolving this constraint is trivial. All that is needed is to sum the 4 mass values and compare them to the mass limit. We are going to use this simple example to illustrate how SysML v2 constraints map to Imandra’s verification goals. Here is the simple mass verification goal in Imandra.
We synthesized the part_masses function by crawling the part hierarchy and identifying all the massed parts. We include the part masses and the multiplicity. The multiplicity is the number of parts of a specific kind, often, it is 1, but not always. In the case of the “traffic_light” model the light_insert has a multiplicity of 3, one light_insert for each light. We need to multiply the part mass by the multiplicity to get the total mass.
The “sa” variable includes all the attributes for the system and the SysML v2 state. The “sa” variable provides a complete view of the entire system at a point in time.
This trivial example shows the mapping from SysML v2 to IML. The verify function explores the entire state space of the system and proves that the goal is met for all undefined variables and values. This verification goal returns Proved.
Formally Verifying a Power Consumption Constraint
We now will apply these techniques to a much more complicated example: power consumption. Power consumption, or power usage, is more complex because power consumption changes during operation. The power constraint seems simple enough and is very similar to the mass constraint definition.
constraint def PowerConstraint {
in partPowers : PowerValue[0..*];
in powerLimit : PowerValue;
sum(partPowers) <= powerLimit
}
assert constraint powerConstraint : PowerConstraint {
in partPower = (light_housing.light_inserts.green_light.power_usage,
light_housing.light_inserts.yellow_light.power_usage,
light_housing.light_inserts.red_light.power_usage,
light_housing.light_electronic_housing.power_usage,
traffic_light_controller.power_usage,
traffic_light_counter.power_usage,
traffic_light_radio.power_usage);
in powerLimit = 19.0 [W];The lights and the radio have a variable power determined by their individual states. In SysML v2 we represented these variable power values as a calculation.
calc def Light_power { in light_state : Light_state;
return : PowerValue =
if light_state == Light_state::off ? 0 [W]
else if light_state == Light_state::lit ? 12 [W]
else if light_state == Light_state::blinking ? 8 [W]
else 0 [W];
}
calc def Radio_power { in radio_on : Boolean;
return : PowerValue =
if radio_on ? 4 [W]
else 1 [W];
}When a light is Lit, it consumes 12 Watts, when it is Blinking, it consumes 8 Watts, and when it is Off, it consumes 0 Watts. The radio consumes 4 Watts when it is transmitting and 1 Watt when it is just listening. Summing up the power of all the components “on” you would get ~43W, well above the constraint.
To verify PowerConstraint, we need to calculate power during operation across all states, all paths, and all possible situations. There are 12 SysML states for the traffic_light system and 45 attributes; you can see the state map below.
It is a more complex process, so we intend to automate most steps and provide high-level configuration tools native to or similar in style and workflow to popular MBSE tools to enable Systems Engineers to efficiently perform these types of inductive formal proofs.
Here are the six steps we follow to formally prove that the power never exceeds 19W:
1. Create a definition for “Good States” for the system.
2. Create a lemma that verifies, that if you start in a “Good State” you will end up in a “Good State” after executing the state machine once.
3. Use the lemma from step 2 to create another lemma that verifies that if you start in a “Good State” you will remain in a “Good State” after executing the state machine an arbitrary number of times using any parameters or values.
4. Define an initial starting point for the system and verify that it is a “Good State”. We used the “Off_state” just after the power was turned on. Now we know that if the system starts from the “Off_state” it remains in a “Good State regardless of how long the state machine runs and over any values and parameters.
5. Create a lemma that proves the power is <=19 Watts for all “Good States”.
6. Use lemmas created in steps 2–5 to verify that if we start from the “Off_state” the system will never exceed 19W regardless of how long it runs and over any values and parameters. Steps 2–6 will be completely automated, so the user will just need to define the “Good States” for the system, which we will make easy through tooling.
Step 1. Define “Good States”
The complete system state is determined by the “SysML_State” and a collection of SysML attributes. The SysML states are shown in the diagram above, and here is the list of the attributes.
The system has 45 attributes in all.
We combine the SysML State and the Attributes into a single variable “sa” of type “sysml_state_attributes”. We then define 12 “Good States” by constraining 8 of these 45 attribute values.
In the “Good States” we confirm the following:
· Power is ON
· The lights are on and off during the appropriate SysML states. Ex. Green Light is “Lit” in the “Green_on” SysML_state and the other lights are “Off”
You will see below that each of the lights is represented twice, once in the controller and once as the light itself. We also define a “Good State” when every light is “Off”, but power is ON.
Step 2. Prove if you start in a “Good State” you remain in a “Good State” after one step of the state machine.
We used this function “good_tl_states” along with the function we developed to execute the state machine to create our first lemma. The “my_step” function executes the state_machine once. It takes a “sa” and returns a new “sa” based on external messages and values, passed as the variable “ex_m”.
The external message “ex_m” is made up of these six variables.
The first lemma “step_good_invariant” proves that if we start in one of our 12 “Good States” we will be in one of the 12 “Good States” after the state machine executes once. We will then use this lemma “step_good_invariant” in the creation of future lemmas.
Step 3. Prove if you start in a “Good State” the system remains in a “Good State” after n steps of the state machine.
Now we create a second lemma that uses the first lemma to verify that if we start in one of our 12 “Good States” we will be in one of the 12 “Good States” after executing an arbitrary list of “external_messages” of an arbitrary length. So no matter how long the state machine runs, we will be in a “Good State”.
The function below “run_my_step” is a recursive function that runs “my_step” once for every element in the list of “external_messages” “ms”. For the lemma, “run_good_invariant” we do not specify the values or the length of the list of “external_messages” to instruct Imandra to prove that if we start in a “Good State” we end in a “Good State” for an arbitrary list of “external_messages” of an arbitrary length.
This lemma “run_good_invariant” also comes back as proved, and we can use it in future proofs.
Step 4. Define an initial state and prove the system remains in a “Good State” after n steps in the state machine.
Next, we defined an initial system state that is in the “SysML_state” = “Off_state” and all the lights are OFF and the Power is ON.
Then we create a third lemma that proves that if we start from the initial SysML state Off_state we will remain in a “Good State” for an arbitrary list of “external_messages” of an arbitrary length.
Step 5. Prove the power constraint is met for all “Good States”
Now we bring in the power calculations. We created a function based on the SysML v2 constraint and used it in our next lemma. The function is “sum_total_power_states” and can be seen below.
We use the above function to prove that the power is <19W for all “Good States”.
Step 6. Prove the power constraint is always met.
It returns proved, and now we are ready for the final step. We use all four of the previously proved lemmas to prove that the power consumption is <19W for an arbitrary list of “external_messages” of an arbitrary length starting from turning the power on.
Theorem proved! The SysML v2 power constraint is true for every possible system state and attribute value.
Conclusion
I am excited about our progress, but we are just getting started. The approach outlined in this article can be done manually today to verify your own SysML v2 models, but we are working to make that process much easier. Here is a short list of work underway:
· Creating a transpiler to use the SysML v2 API to export SysML v2 models as JSON and automatically convert them to IML.
· Developing tooling and automation to accelerate formal verification of SysML v2 constraints.
· Integrating Imandra Automated Reasoning Engine with Large Language Models to enable a hallucination-free natural language interface for reasoning about your SysML v2 models, creating verification goals, and synthesizing SysML v2.
To discuss this work, please contact me at Jamie@imandra.ai, or look for me at the next OMG members meeting.
