Coverting Logic to CertSAFE Models Tutorial

Immutable variables

In standard imperative languages, variables are usually mutable. This means you can create the variable and then write a value to it multiple times. With this type of variable, when you read from it its value will be the value that was last written to it. This can lead to problems figuring out what the value of a variable should be in many cases as it is not always simple to figure out what may have written to it last or what it may have calculated when it did. Also with this classic imperative style variable, the variable continues to live on until the compiler knows it can guarantee the variable will no longer be used, which can result in the variable persisting for the entire runtime of the software.

In CertSAFE, the behavior and lifecycle of a variable is quite different. CertSAFE variables are all immutable, and no variable is ever persisted beyond the end of a frame of execution. This means that a variable can only be written to once, at the time it is initialized, and never again. It also means it will be discarded sometime after it will no longer be used for this frame and before the execution of the next frame. Because of this, at the beginning of each frame none of the variables have been initialized; as the frame executes, each variable will be initialized and set to a value only one time, then it will be read by anything in the frame of execution that uses it, and finally it will be discarded before the next frame of execution.

Understanding the behavior of variables in CertSAFE and how they differ from imperative languages is important, as there are considerations that must be kept in mind when translating between the two. Also, understanding this behavior can greatly simplify the reasoning necessary to understand what is happening with a given variable.

State

In standard imperative languages, state is often handled with mutable variables that persist for the period of time the state is required, which can be as long as the entire runtime of the software. However the nature of CertSAFE’s variables prevents a variable from persisting longer than a frame or changing values once it is set. This requires CertSAFE to handle state rather differently. In CertSAFE the variable itself cannot hold a value past a frame boundary, so we use the one frame delay to persist the actual value past the frame border. Most imperative code and design involves heavily utilizing mutable variables. This presents several challenges when converting from imperative styled requirements or pseudocode to CertSAFE, which does not allow any mutable variables.

Breaking up variables

When a variable is mutable, any requirement may write to it. This means a given variable may have a variety of different values during a single frame of execution, and any requirement that reads from it could be reading any one of those various values depending on when it reads from the variable as the variable is being changed by different requirements. To illustrate this more clearly, let’s consider the following requirements.

Table 1 Original Requirements
2.1.8 if Condition 2 then A = 0
2.2.2 if Condition 3 then A = A * 3
2.2.3 if Condition 3 is not true then A = A - 5
2.4.8 if Condition 1 then A = A + 1 else A = A - 1
2.6.7 C = A * 12
3.5.8 A = 0
3.5.10 B = A * 12

These requirements represent all of the requirements that reference the variable A in a hypothetical requirements document. You may notice that many of the requirements write to A. So, when a requirement reads from A, what value is it reading? This question often cannot be answered without additional information. In this example we will assume that an engineer has read over the document and was able to find out that the requirements would always be executed in a specific order, and that order is as follows.

Table 2 Reordered Requirements
3.5.8 A = 0
3.5.10 B = A * 12
2.4.8 if Condition 1 then A = A + 1 else A = A - 1
2.2.2 if Condition 3 then A = A * 3
2.2.3 if Condition 3 is not true then A = A - 5
2.1.8 if Condition 2 then A = 0
2.6.7 C = A * 12

Now with that extra information, it is clear how to calculate what the value of A should be when any given requirement reads from it, thus this is enough information to know what the system is supposed to do. However, we still have the problem that in CertSAFE we only have immutable variables so we cannot write to A more than once. The solution is to create separate variables for each state that A will be in. While doing this it is important to consider what the result of an if statement without an else clause will be. This is important as we often use switches to represent if statements in CertSAFE, however that is not the best mapping since switches always perform an assignment and always need an else clause. When possible, converting if statements to ternary operators can often make the translation clearer. Using this technique, the requirements can be represented as follows.

Table 3 Broken Up Requirements
3.5.8 A [Initial] = 0
3.5.10 B = A [Initial] * 12
2.4.8 A [Step 1] = Condition 1 ? A [Initial] + 1 : A [Initial] - 1
2.2.2-3 A [Step 2] = Condition 3 ? A [Step 1] * 3 : A [Step 1] - 5
2.1.8 A [Final] = Condition 2 ? 0 : A [Step 2]
2.6.7 C = A [Final] * 12

Now we have the lifecycle of the variable broken into stages representing its intermediate states. From here it is straightforward to diagram the requirements. All of the requirements that wrote to A can be placed in a single diagram with only the states read by other requirements exported. This is not necessary, but it does keep things a bit cleaner.

../_images/Conversion-Breaking-Up-A-1.png
../_images/Conversion-Breaking-Up-A-2.png
../_images/Conversion-Breaking-Up-A-3.png
../_images/Conversion-Breaking-Up-A-4.png

Fig. 1 Calculate A.cxdiag

For the remainder of the requirements, each requirement can be placed in its own diagram. Again, this is not necessary, but it is one reasonable choice.

../_images/Conversion-Using-A-Part-1.png

Fig. 2 Calculate B.cxdiag

../_images/Conversion-Using-A-Part-2.png

Fig. 3 Calculate C.cxdiag

Execution order

In standard imperative languages, execution order is fairly straightforward to follow. Each line executes in order until one calls another function, then execution jumps to the called function, followed by returning where it left off once the function completes. However, this behavior is not always guaranteed as it can be circumvented with interrupts, and is often difficult or impossible to trace backwards from any given spot in the code.

In CertSAFE, order of execution works differently. Unlike with imperative languages, there is no specific order of execution—there are just data dependencies and a guarantee that any instance of a unit (function) will not run until all of the variables it is dependent on have already been populated.

Conditional execution

In standard imperative languages, given blocks of code may be skipped in the execution based on conditions. The if-then statement is the most common and simplest example of conditional execution. In this case, if the given condition is met then the block of code is executed, otherwise it is skipped over.

In CertSAFE, there is currently no form of conditional execution. This means that everything is executed every frame. A common method for handling if-then-else statements that set variables is to simply use a switch; however, this method does not always work. Consider the following simple pseudocode.

if Condition then
  A = A + 1
  Result = A
else
  Result = A
endif

A naive implementation of the above code might look like the following.

../_images/Conversion-Bad-If.png

Fig. 4 Bad If.cxdiag

However, the problem is that in this case the A = A + 1 portion of the diagram is executed even when Condition is false. It would not have executed in an imperative language because the if part of the if-then-else conditional statement would not have executed. This wouldn’t be a problem if the variable A didn’t maintain state, however since it does that state will continue to be changed even when Condition is false. One way to fix this is to make the updating of the state conditional. For example, we can create a Conditional Delay custom component that will hold its value if a condition is false or act as a One Frame Delay if it is true, similar to the following.

../_images/Conversion-Conditional-Delay-Implementation.png

Fig. 5 Conditional Delay Implementation.cxdiag

Then we can replace the original One Frame Delay with a Conditional Delay and run Condition to it, as shown below. Now the state will only be updated when Condition is true.

../_images/Conversion-Good-If.png

Fig. 6 Good If.cxdiag

This isn’t a perfect match to the structure of the original pseudocode, as it implements something more like the following.

A′ = A + 1
Result = Condition ? A′ : A
A = Condition ? A′ : A

However, this is not a problem, as A still correctly retains its previous value when Condition is false.

Unfolding variables

Sometimes you may see a requirement of the following form.

BlahX shall be incremented by ThingY where X = [Unit1, Unit2, Unit3] and Y = [Front1, Left1, Right1] respectively.

Here, the intent of the requirement was to represent the same action being taken on various pairings of variables. These requirements can be seen as a collapsing of several requirements into a single one. Expanding the variables out into all of their full names, the above would look like the following.

BlahUnit1 shall be incremented by ThingFront1
BlahUnit2 shall be incremented by ThingLeft1
BlahUnit3 shall be incremented by ThingRight1

We can save a lot of time by taking the generic logic that is repeated and defining it in its own diagram. For example, in this case we would have something like the following.

../_images/Conversion-Increment-By.png

Fig. 7 Increment By.cxdiag

This gives us a model of the generic requirement. In order to use this generic requirement in the model, we need to map it to all of our expanded variables. This can be accomplished with either a diagram or a stitch and CertSAFE’s reuse features by creating an instance of the generic logic for each pair. For this simple case we will use a diagram. The resulting diagram is as follows.

../_images/Conversion-Unfolding-Variables.png

Fig. 8 Unfolding Variables.cxdiag

For logic with a particularly regular structure, it may be possible to simplify the notation further by using CertSAFE’s blocks features and representing the variables as enum-indexed arrays. See the Blocks and Arrays Tutorial for an introduction to working with arrays in CertSAFE.