Automated Reasoning for SysML v2 Part 3
Using Imandra Region Decomposition to Gain Insights of SysML v2 Models.
The team at Imandra is continuing to develop techniques and explore how Imandra Automated Reasoning can provide insights and prove properties of SysML v2 models. This is the third article in a series on how to use Imandra with SysML v2. In the prior two articles, we covered how Imandra Automated Reasoning is used to verify and prove the correctness of systems. We will expand the Automated Reasoning discussion in this article by looking deeper at proving determinism using formal methods.
Specifically, in the prior two articles, we covered formally verifying two different types of verification goals for a traffic light. In article one, we proved that the system properly handled errors and placed the systems in an operational “stop_sign” mode if an error was detected. We proved that the system would fail-operational and notify the central office of the error via an SMS message. In the second article, we used Imandra Automated Reasoning to prove SysML v2 constraints and requirements are always met.
I recommend that if you have not read those two articles, please do so; they are linked in medium.com at the bottom of this article. For those of you who have read them, thank you. I am very interested in your thoughts and feedback.
Using Imandra Automated Reasoning with SysML v2.
SysML v2 is a general-purpose modeling language for complex system design. SysML v2 is an open standard developed by the Object Management Group (OMG). Our work at Imandra is based on the SysML v2 pilot implementation and beta release from July 2023. The OMG working groups continue progressing toward a final release, which should come in mid-2024. For more information on the SysML v2 release schedule, go to omg.org.
We have spent several months learning SysML v2 and mapping the semantics to Imandra Modeling Language (IML). The more we learn, develop, and experiment, the more excited we get about the potential. The SysML v2 formal semantics will allow us to use Imandra Automated Reasoning in a wide range of applications to help systems engineers design safer systems faster.
At Imandra, we are executing against a roadmap that includes the following:
· Formal verification of properties, requirements, and constraints.
· Conversion from SysML v1 to SysML v2
· SysML v2 to IML transpiler
· Hallucination-free natural language interfaces (ChatBots) will enable all stakeholders to explore and reason about SysML v2 models.
· Integration with popular MBSE development tools
In this article, we will continue to use the traffic light model discussed in the previous two articles. We will show how to use Imandra Automated Reasoning to prove the determinism of the state machine. We will also introduce you to region decomposition to explore all the behavioral regions of the SysML v2 model and to create a semantic diff.
SysML v2 State Machines, States, and Transitions
SysML v2 system behavioral flow is done primarily in two ways. Systems engineers use SysML v2 to model behavior with action nodes and control nodes, such as forks, joins, merge, and decision. The other approach is state-based behavior using a state machine. Both approaches model complex behaviors, and of course, these two approaches can be combined side-by-side or in a hierarchy. This article will focus solely on state-based behavior and state machines.
SysML v2 state machines have three basic elements: states, transitions, and actions. States invoke actions, and transitions determine when you change states. SysML v2 states are a specialized type of action that calls up to three sub-actions: an Entry-action, a Do-action, and an Exit-action. Of course, actions can call additional actions, so you are not limited to only three actions, but there are three events when the actions are invoked. The Entry-action is executed when you enter the state, and then the Do-action is executed after the Entry-action is complete. The Exit-action is executed when the state transitions to another state.
The SysML v2 transitions determine when the state machine changes from one state to another. The SysML v2 transitions may have guards that are expressions that return a Boolean value. If the Boolean value is true, then the transition criteria are met, and the state changes to another state dictated by the transition. Here is a simple diagram of the order of execution of states and actions determined by SysML v2 transitions.
One case that can be confusing is what happens if a transition criterion is met before the Do-action is complete. If that occurs, the Do-action is terminated, and the Exit-action is executed.
To help us better understand SysML v2 state machines, I will go through the traffic light example in some detail. The traffic light state machine has 12 states and 18 transitions. The states are blocks in the state diagram below, and the transitions are arrows. While this state machine is not trivial, it is pretty simple. In the next section, let’s look at a few states and the transitions, first in SysML v2 textual notation and then in Imandra Modeling Language (IML).
Explaining the Traffic Light State Machine
Let’s look at a section of the state machine to help explain SysML v2 state machine concepts and lay the foundation for our discussion of determinism later in the article. We will detail a few states, transitions, and actions to help us understand SysML v2 state machines. This will lead to our explanation of how Imandra Automated Reasoning proves determinism and isolates design errors in the state machine.
The path from “traffic_flow” to “yellow_on” of the state machine has four states (traffic_flow, red_on, green_on, and yellow_on) and five transitions and two additional transitions between “traffic_flow” and “operation_selection.” We will start with the transitions to show how the state machine determines when to change from one state to another. Below is the SysML v2 textual notation for the transitions “traffic_flow_to_red_on” and “traffic_flow_to_operation_selection.”
transition traffic_flow_to_red_on
first traffic_flow
accept when (traffic_light_controller.error == false)
then red_on;
transition traffic_flow_to_operation_selection
first traffic_flow
accept when ((traffic_light_controller.message_queue != "")
or (traffic_light_controller.error == true))
then operation_selection;These two transitions are simple and self-explanatory. If the state machine is in the “traffic_flow” state and an error has not been detected, the system will transition to “red_on.” If the state machine is in “traffic_flow” and there is an error, OR if there is an external message, the system will transition to “operation_selection.” In “operation_selection” the system may change its operating mode or if an error occurred continue toward the “diagnostic” state.
Now let’s look at the “traffic_flow” state.
state traffic_flow {
entry traffic_light_controller.check_status;
exit;
}The “traffic_flow” state has an entry function “check_status,” which updates both the “Error” Boolean and the “message_queue.” “Error” and “message_queue” are both used to evaluate the “traffic_flow” transitions. To summarize “traffic_flow,” we have an action that updates the attributes the transitions use to trigger transitions to one of two different states. This example is about as simple as it gets. Now let’s move on to the “red_on” state.
The “red_on” state also has two transitions. They are more complex but still a series of Boolean expressions. We will go over the two transitions one at a time. Below is the “red_on_to_green_on” transition.
transition red_on_to_green_on
first red_on
accept when ((traffic_light_controller.wait_duration >traffic_light_controller.red_on_time)
and (vehicle_sensor.vehicle_at_light == true)
and (traffic_light_controller.message_queue == "Safe_all_red"))
then green_on;This transition is easy to read from top to bottom. The state machine will change from the “red_on” state to the “green_on” state if the system has been red longer than the “red_on_time” AND there is a vehicle waiting at the red light, AND we have received the safety message that all the other lights at the intersection are red.
The other transition usage, red_on_to_traffic_flow, is below.
transition red_on_to_traffic_flow
first red_on
accept when ((((traffic_light_controller.message_queue != "")
and (traffic_light_controller.message_queue != "Safe_all_red"))
or (traffic_light_controller.error == true)))
then traffic_flow;The state machine transitions from the “red_on” state to the “traffic_flow” state when there is an external message AND that is not “Safe_all_red” OR if an error has been detected. This is similar to the conditions that change the state machine from the “traffic_flow” state to the “operation_selection” state.
The “red_on” state has actions that impact the traffic light beyond the execution of the state machine. The “red_on” state has an entry function, “turn_red_on,” that handles turning lights off, resetting the wait clock, and changing the state of the red_light to “lit.”
[NOTE: The :>> is redefine syntax in SysML v2.]
state red_on {
entry traffic_light_controller.turn_red_on;
do traffic_light_controller.check_status;
exit;
}
action turn_red_on {
perform action turn_lights_off;
perform action reset_wait_clock;
attribute :>> traffic_light_controller.red_light_state = Light_state::lit;
}The states and transitions usages for the states “green_on” and “yellow_on” are similar to “red_on.” The SysML v2 textual representation is included below, but we will not walk through them. One difference is that the “green_on” and the “yellow_on” states have only one transition.
transition green_on_to_yellow_on
first green_on
accept when (traffic_light_controller.wait_duration > traffic_light_controller.green_on_time
or (traffic_light_controller.error == true))
then yellow_on;
transition yellow_on_to_red_on
first yellow_on
accept when ((traffic_light_controller.wait_duration > traffic_light_controller.yellow_on_time))
then red_on;
state green_on {
entry traffic_light_controller.turn_green_on;
do traffic_light_controller.check_status;
exit;
}
state yellow_on {
entry traffic_light_controller.turn_yellow_on;
do traffic_light_controller.check_status;
exit;
}For those of you newer to SysML v2, I hope you better understand SysML v2 state machines, including their states and transitions. In the next section, we will use Imandra Automated Reasoning to prove that the state machine is deterministic, which means that each state has either zero or one legal transition at any time.
State Machine Determinism
We will go over how Imandra Automated Reasoning is used to prove the determinism of a SysML v2 state machine. We can use similar techniques to prove other properties, including but not limited to “reachability” and “no-dead-lock.” Reachability is proving that each state in the state machine can be reached. “No-dead-lock” proves that the state machine will not become stuck in a state and unable to change states.
To use Imandra Automated Reasoning, we must convert the SysML v2 model to IML. We have been doing these conversions manually but are actively developing a transpiler to convert from SysML v2 to IML automatically.
The traffic light SysML v2 model has 12 states, 18 transition usages, and 45 attributes. Some of the attributes are discrete, like “error,” and some are continuous, like “wait_duration,” and some are enumerated types, like the “external_messages.” To prove determinism of the state machine, we will focus on the 18 transitions. Let’s take a look a two of the transition converted to IML. The transitions “traffic_flow_to_red_on” and “red_on_to_green_on” in IML are similar to their SysML v2 textual representation.
IML is based on the open-source language OCaml, and IML is nearly identical to OCaml. IML is a slightly scoped version of OCaml to ensure we can use all the Imandra Automated Reasoning tools. It is trivial for developers to include OCaml and OCaml libraries in Imandra if needed for visualization or data manipulation.
In IML, we represent the two transition usages as functions with one parameter, “sa.” “sa” is a variable containing the current SysML state and all 45 system attributes. When we convert the model to IML, we define a type “sysml_state_attributes” and then declare a variable “sa” of type “sysml_state_attributes.”
When we evaluate a transition in IML we pass in “sa” and resolve the Boolean logic. If the Boolean logic resolves as “true,” we change the SysML state; if not, we return “sa” unchanged.
We have converted all 18 SysML v2 transition usages to IML functions. To prove that the state machine is deterministic, we will create a helper function called “check_state_transition_functions” that takes a single parameter, “sa.” “check_state_transition_functions” checks each transition function, in turn, using the same “sa.” Every time a transition evaluates to true, we increment a variable “i” by 1. If no transition functions are satisfied, “check_state_transition_functions” will return “0”; if one and only one is satisfied, it will return “1”; and if more than one transition function is satisfied, it will return “>=2”. For a state machine to be deterministic, this function must return “0” or “1” for all SysML States and all attribute values.
We will use “check_state_transition_functions” in an Imandra verify function to prove that either 0 OR 1 transition usage satisfies all values of “sa.” Imandra Automated Reasoning will evaluate all 18 transition usages, all 12 SysML states, and all 45 attributes simultaneously and mathematically prove that “check_state_transition_functions” returns either “0” OR “1”.
Those who were paying close attention in the prior sections may have noticed that this verification cannot be proved due to a lack of constraints in the transitions. Two issues prevent the proof. When “verify” is called, Imandra returns Refuted and a Counter Example showing an explicit “sa” that caused the proof to fail. I trimmed down each counter-example to the relevant attributes. I will go through them one at a time.
When the state machine is in the “Traffic_flow” state AND the “error = false” AND there is a message in the message queue, it is ambiguous whether the state machine should transition to the state “Operation_selection” or “Red_on.” We can correct this issue by modifying “traffic_light_to_red_on” by adding a specific check that no messages are in the message queue.
Now, let’s look at the second issue, which is a significant safety concern.
When the system is in the SysML state “Red_on,” and there is an error, and we have received the message “Safe_all_red,” indicating that all of the other lights at the intersection are red, it is unclear whether the system should change to the “Green_on” state or to the “Traffic_flow” state, as both transition functions are satisfied. This is an issue and potentially a significant safety concern because we do not want to turn the light green if we detect an error in the system.
The ambiguity can quickly be addressed by adding “error = false” to the “red_on_to_green_on” transition usage.
Once we correct both issues in the transition functions, we can re-run the verify function, and it returns “Proved” and provides formal proof for review and confirmation by third-party proof checkers.
If you already saw these issues when reading the previous section. Good for you! The two bugs were in my SysML v2 model of the traffic light when I wrote it and converted it to IML. One of the reasons mistakes and bugs are so common is that systems are getting increasingly complex. Even this simple model of a traffic light has a surprising number of behavioral regions.
Region Decomposition
We can use Imandra Region Decomposition to create a map of any function in our IML model. The result is a collection of invariant regions that collectively represent the entire behavior of the function or system. IML has tools for executing the SysML v2 state machine, including a function for evaluating transitions, “transition sa.” “Transition sa” evaluates transition in every iteration of our state machine engine, checking if any transition expression returns true and, if so, changing the SysML v2 state. Below, we use Imandra Region Decomposition to provide a complete map of the function “transition sa.”
For the traffic light state machine, the transitions represent 175 unique behavioral regions. Each one of these regions represents a collection of constraints that determine an invariant result. We represent the regions in an interactive Voronoi diagram to allow users to explore the state space. The diagram above highlights the region where the power is off, and the invariant result is that we are in the SysML Off_state. The other 174 regions are when the power is ON. Let’s look at two of them.
This is one of the two regions we corrected. It is when the conditions for the transition “red_on_to_traffic_flow” are met. In the constraints, you will see that the power is “on” AND message is “Safe_all_red” AND there is an error. So, the SysML State is changed to “Traffic_flow.” It will then progress toward the “diagnostic” state.
Below is the other corrected transition, “traffic_flow_to_red_on,” where power is on AND no error AND no external message. In this region, the SysML State changes to “Red_on.”
Constraining Region Decomposition and Semantic Diffs
Region decomposition is a powerful tool, but sometimes, you want to reduce the number of results by a specific outcome or condition. We can add helper functions to set conditions for the region decomposition. Here are three sets of constraints and the corresponding results.
The first function we use to set a condition is “sysml_state_red_on sa.” It returns a Boolean true if the SysML v2 State starts in “Red_on” and transitions to any other SysML v2 State.
The “sysml_state_red_on sa” function is applied as a condition using the syntax ~assuming:”sysml_state_red_on.” The result is a collection of 14 regions, where one region is a transition to “Off_state,” another region is a transition to “Green_on,” and the other 12 are different sets of constraints that change from “Red_on” to “Traffic_flow.”
Sometimes, you may want to see the path to a specific state, not the destinations from a starting state. This is called a preimage. We can easily generate a preimage using region decomposition. To do so, we will create another condition function. The “sysml_end_green_on sa” function returns a Boolean true if the system changes from any SysML v2 State to the SysML v2 State “Green_on.”
This Region Decomposition returns only one region, which means that we have one, and only one, path that ends with the SysML v2 State “Green_on.” This result is exciting because we show no unexpected edge cases will lead to a “Green_on” state.
The final thing to look at is the Semantic Diff between the transitions before and after we corrected them. Here is the third and final function we will use as conditions for the Region Decomposition.
“diff_t” returns a Boolean true if the transition functions have different results for a given “sa.” The notation of M3 and M2 refer to different modules, or namespaces, in IML. By declaring the function transition in different modules, they can have different definitions and behavior but the same name. We then use Region Decomposition on the function “M3.transition” with the condition that “M2.transition <> M3.transition”. The “M2.transition” is the collection of transition usages before we corrected the mistakes we found in the earlier section, and the “M3.transition” is after we made the corrections.
This is a semantic diff between the two instances of the transition function. We see only two regions; one reflects the changes we made in the transition usage “red_on_to_traffic_flow,” and the other reflects the changes we made to “traffic_flow_to_operation_selection.”
Conclusion
We continue to make progress and expose more ways to leverage Imandra to reason about SysML v2 models. Determinism, reachability, dead-lock preventions, and semantic diffs are just examples of what is possible. I am excited to learn from you what type of analysis and reasoning would help your teams and customers be more successful systems engineers and stakeholders. We should have the first version of the SysML v2 to IML transpiler done in early 2024 and we would like to get access to your examples to test it. We also want to speak to SysML v1 end-users interested in automatic conversion to SysML v2. Please get in touch with me at Jamie@imandra.ai or look for me at the next OMG members meeting.
