This site uses cookies for analytics, personalized content and ads. By continuing to browse this site, you agree to this use. Learn more

*SAML* (**S**ystem **A**nalysis **M**odelling **L**anguage) was developed at the Chair of Software Engineering at the Otto-von-Guericke University Magdeburg.
It enables users to perform formal safety analysis for safety critical system.
This tutorial will show you some basics the capabilities of *SAML*.
More tutorials can be found on trysaml.org.
If you want to download *SAML*, visit our website.

Be sure to follow along with the examples by clicking the "*load in editor*" button.
See what the *SAML* verification engine says, try your own models and experiment!

Safety analysis is an important focus in safety critical systems.
Model-Based safety analysis aims at finding the causal connections between component malfunctioning and overall system hazards based on mathematical deduction techniques.
Two different types of safety analysis tools can be distinguished.
It can be qualitative, with two-valued logic or quantitative where probabilities are computed for logical properties.
For both, there exist elaborate verification tools (like PRISM, NuSMV, MRMC, SPIN, ...) and corresponding formalization logic's.
In common for all tools is the need of a formal model.
These models have to be built separately for each verification tool which is potentially very time-consuming and error-prone.
Thus *SAML* aims to unify the development and verification of qualitative and quantitative formal models.

*SAML* can be used for both qualitative and quantitative analyses and allows the combination of discrete probability distributions and non-determinism.
In *SAML*, a model describes finite state automata that are executed in a synchronous parallel fashion with discrete time steps.
The language has been explicitly designed as simple as possible, while being expressible enough for convenient modeling of large systems.
Indeed the language is capable to cover the functional model as well as the failure model.
It is also possible to create an environmental model to be able to model reactive systems.

In *SAML*, the function and behavior in a formal model is specified in **state transitions**.
Thus the duty of the modeler is to specify every state transition of the system, which is relevant for the according safety check.
The following sections will give you an overview on some elements in *SAML*.

Besides the pure definition of state transition an important feature of state-of-the-art verification tools is the ability to cluster states into components.
Thus every formal model in *SAML* is clustered into **components**.
Components represent an finite state automata.
Thus multiple hierarchically clustered components represent a product automat.

The following example will give you a brief overview on the syntax for specifying components in *SAML*.
Note that components are always specified with an identifier.

```
component nameOfTheComponent
...
endcomponent
```

For clarity proposes these components can recursively contain any number of sub-components. Grouping parts of a model into sub-components can greatly improve the readability, because it helps clarifying the relations between components. The following example will show you the syntax for nesting components.

```
component parentComponent
component firstChildComponent
...
endcomponent
component anotherChildComponent
...
endcomponent
endcomponent
```

Through the ability to specify components and nested components, *SAML* gives you the opportunity to add structure to your model.
This allows you to model even more complex systems.
However if you do just specify the componential structure, you are missing the most important part in formal model checking: *states*.

In *SAML*, its essentiall to specify states.
Those states will be wrapped inside components.
States represent properties of their parent components.
In the following example we will show you how to initialize a state called `stateName`

which's value can range from `0`

to `10`

and is initialized with `1`

.

```
component stateInitialization
stateName : [0..10] init 1;
...
endcomponent
```

Besides the pure initialization of a state it is moreover important to specify the transitions of states.
If you do look at this example, you will notice, that the value of `stateName`

will never change.
But if we do want the value to be changed over time steps, we do have to specify update rules.
Update rules have to be defined with the following syntax:

```
component stateTransition
stateName : [0..10] init 1;
stateName = 0 -> stateName' = 0;
stateName > 0 & stateName < 10 -> stateName' = stateName + 1;
stateName = 10 -> stateName' = 10;
endcomponent
```

In this example, we reuse the state `stateName`

.
The first update rule specifies that if the current value of `stateName`

equals `0`

, the following value will be also `0`

.
The next update rule specifies the rest of the behavior, if the value is greater than `0`

and less then `10`

, it is incremented by `1`

.
The last update rule specifies the same behavior as the first rule, thus if the value of `stateName`

equals `10`

, it will remain at `10`

.

If you do specify update rules in *SAML*, you do have to keep some important aspects in mind:

**Every discrete time step, all update rules are evaluated atomically.**Therefore if you do change values of states, be aware that all changes will be applied within on atomic step.**In every step exactly one update rule has to be active.**Therefore you do have to make sure that no other update rule might overrides your intended condition.**Update rules have to be defined in an exhaustive way.**You have to specify every possible state transition. Even though if some transitions might be unreachable.**Update rules have to be completely specified.**You do have to define the next values of all states within every update rule.

Lets recap those aspects and apply them to our model stated above.
If you look at this example, you will notice that the first update rule will actually never be applied.
Nevertheless it has to be specified.
Looking at the second update rule we keep in mind, that `stateName < 10`

is necessary else our model will produce unwanted behavior.
The last update rules completes our small example.
Hence we do have a fully functional simple model.

Until now you are capable of the basics in *SAML*.
We have shown how to specify states, update rules and components enabling you to easily build even complex formal models.
Hence we can now start to examine the basics in verifying those models.

Formal model checking in *SAML* means to verify given specifications.
In *SAML*, specifications are declared trough `NUSMVSPEC`

s or `PRISMSPEC`

s.
In order to remain as comprehensible as possible, we will reuse the example from above.
Thus the following model should look pretty familiar to you:

```
component modelToCheck
stateName : [0..10] init 1;
stateName = 0 -> stateName' = 0;
stateName > 0 & stateName < 10 -> stateName' = stateName + 1;
stateName = 10 -> stateName' = 10;
endcomponent
//There EXISTS GLOBALLY at least one state
// at any point in time where stateName equals 0?
NUSMVSPEC EG (stateName = 0);
//There EXISTS FINALLY at least one state
//at any point of time where stateName equals 10?
NUSMVSPEC EF (stateName = 10);
```

As you might have noticed, we changed the current name of our component to `modelToCheck`

, which is just relevant for representational aspects.
Additionally we added two specifications.
As *SAML* aims to support multiple formal model checkers, we need to specify which one we actually want to use.
We chose NuSMV by using the `NUSMVSPEC`

keyword.
Currently *SAML* supports two different model checkers: NuSMV and PRISM.
The syntax for specifications changes according to the model checker.
Lets dig into the basics of NuSMV and PRISM.

Specifications for NuSMV allows you to perform qualitative formal model checking.
NUSMV specifications in *SAML* basically consist of the `NUSMVSPEC`

-keyword, boolean expressions or **C**omputation **T**ree **L**ogic expressions. Thus they are specified trough the following syntax:

- NUSMVSPEC
**[!]******EG** (`expression`

) - [not]**e**xists**g**lobally - NUSMVSPEC
**[!]******EX** (`expression`

) - [not]**e**xists ne**x**t state - NUSMVSPEC
**[!]******EF** (`expression`

) - [not]**e**xists**f**inally - NUSMVSPEC
**[!]******AG** (`expression`

) - [not] for**a**ll**g**lobally - NUSMVSPEC
**[!]******AX** (`expression`

) - [not] for**a**ll ne**x**t state - NUSMVSPEC
**[!]******AF** (`expression`

) - [not] for**a**ll**f**inally - NUSMVSPEC
**[!]******E** (`expression`

**U**`expression`

) - [not]**e**xists**u**ntil - NUSMVSPEC
**[!]******A** (`expression`

**U**`expression`

) - [not] for**a**ll**u**ntil

These `expressions`

can contain other CTL expressions or simple logical expressions using the following logical elements:

**!**- logical not**&**- logical and**|**- logical or**xor**- logical exclusive or**xnor**- logical not exclusive or**->**- logical implies**<->**- logical equivalence

For further information on CTL expressions either consult our documentation or visit the documentation of NuSMV.

If you want to use a quantitative model checker like PRISM you have to use `PRISMSPEC`

.
Like `NUSMVSPEC`

s they are specified trough the following syntax:

- PRISMSPEC
**P****[**`min`

**|**`max`

**]****(**`=`

**|**`<`

**|**`<=`

**|**`>`

**|**`=>`

**)****(**`x`

|`?`

**)****(**`expression`

**)**

As you will notice this syntax is closely related to the original PRISM syntax.
According to the documentation of PRISM, the `P`

operator is also used to reason about the probability of an events occurrence in *SAML*.
Thus it is possible to specify a bound using `=`

, `<`

, `<=`

, `>`

or `=>`

.
The `x`

operator has to be replaced with a probability ranging from `0`

to `1`

.
PRISM will then compute, if the probability is within that bound.
In addition to `P`

it is possible to specify `Pmin`

or `Pmax`

in combination with `?`

.
In that case, PRISM will compute the minimum and respectively maximum probability of the occurce of the given `expression`

.
In *SAML* `expression`

can be any kind of CTL expression or any simple boolean expression.

*SAML* owns many features to make formal model checking easier.
One example how *SAML* changes the game are **enumerations**.
Enumerations represent human readable values of states.
A common example for `enums`

are traffic lights.
But before we are digging into that example, we want to show you our motivations to include `enums`

into *SAML*.

The following examples shows a common traffic light:

```
component trafficLightBadPractice
color: [0..2] init 2;
color = 2 -> color' = 0;
color = 0 -> color' = 1;
color = 1 -> color' = 2;
endcomponent
```

As you do see it is hard to estimate what number equals what color.
Therefore you will have to guess in what state the traffic light is initialized for example.
This example easily shows our motivations for adding human readable enumerations to *SAML*.
The following example will show you how to use `enums`

practically.

```
enum trafficLightColors := [green, yellow, red];
component trafficLightBestPractice
color: trafficLightColors init red;
color = red -> color' = green;
color = green -> color' = yellow;
color = yellow -> color' = red;
endcomponent
```

This example is much more human readable. It is easy to determine in what state the traffic light is initialized.

As in the example above, one might want to argue that the color of a traffic light does not switch from red to green. Actually it changes from red to yellow and from yellow to green. Thus one might want to add the following state transition:

```
enum trafficLightColors := [green, yellow, red];
component trafficLightNotFunctional
color: trafficLightColors init green;
color = red -> color' = yellow;
color = yellow -> color' = green; //Error
color = green -> color' = yellow;
color = yellow -> color' = red; //Error
endcomponent
//Does there EXISTS FINALLY at least one state at any point in time
//where trafficLightNotFunctional.color equals red?
NUSMVSPEC EF (trafficLightNotFunctional.color = red);
```

You will see, if you do load this example into the editor and hit the **run** button, that the color of this traffic light will never become red.
As stated in the sections above, this example shows a not exhaustive update rule definition.
But how might we extend our traffic light to reach the intended behavior?

As we have shown in the previous example the naive approach to extend the traffic light example will not behave as intended. Hence we can extend it using an additional enumeration item.

```
enum trafficLightColors := [green, yellowGreen, red, yellowRed];
component trafficLightExtenstion1
color: trafficLightColors init red;
color = red -> color' = yellowRed;
color = yellowRed -> color' = green;
color = green -> color' = yellowGreen;
color = yellowGreen -> color' = red;
endcomponent
//Does there EXISTS FINALLY at least one state at any point in time
//where trafficLightNotFunctional.color equals red?
NUSMVSPEC EF (trafficLightExtenstion1.color = red);
```

You will see, if you do load this example into the editor and hit the **run** button, that the color of this traffic light will become red again.
Trough specifying `yellowGreen`

and `yellowRed`

, it is possible to implicit determine whether the last state before yellow was red or green.
Thus this example will behave as intended.
Besides adding additional enumeration items there are other way to model the intended behavior.

Another practical solution is to add another state variable called `lastColor`

.
This state variable will always contain the color value of the last step, helping the model the determine whether it will switch to red or green.

```
enum trafficLightColors := [green, yellow, red];
component trafficLightExtenstion2
color: trafficLightColors init red;
lastColor: trafficLightColors init yellow;
color = red -> color' = yellow & lastColor' = red;
color = green -> color' = yellow & lastColor' = green;
color = yellow & lastColor = red -> color' = green & lastColor' = yellow;
color = yellow & lastColor = green -> color' = red & lastColor' = yellow;
//state transitions have to be exhaustive
color = yellow & lastColor = yellow -> color' = red & lastColor' = yellow;
endcomponent
//Does there EXISTS FINALLY at least one state at any point in time
//where trafficLightNotFunctional.color equals red?
NUSMVSPEC EF (trafficLightExtenstion2.color = red);
```

This examples represents another way of modeling the exact same system. Nevertheless it is not the most effective way to model a traffic light. This model contains the drawback of an additional unreachable update rule. Using this configuration of enums it is simply not possible to delete the last update rule.

As shown above there are multiple way to the same model.
In the this section we will show you some tweaks to reduce the amount of updates rules you do have to define.
On this background, we define another enum called `lastTrafficLightColors`

.

```
enum trafficLightColors := [green, yellow, red];
enum lastTrafficLightColors := [green, red];
component trafficLightExtenstion3
color: trafficLightColors init red;
lastColor: lastTrafficLightColors init red;
color = red -> color' = yellow & lastColor' = lastTrafficLightColors.red;
color = green -> color' = yellow & lastColor' = lastTrafficLightColors.green;
color = yellow & lastColor = lastTrafficLightColors.red -> color' = green & lastColor' = lastColor;
color = yellow & lastColor = lastTrafficLightColors.green -> color' = red & lastColor' = lastColor;
endcomponent
//Does there EXISTS FINALLY at least one state at any point in time
//where trafficLightNotFunctional.color equals red?
NUSMVSPEC EF (trafficLightExtenstion3.color = trafficLightColors.red);
```

As you see in this example, we have a defined to enums reusing `green`

and `red`

.
Hence we do have an ambiguous definition of the enum values `green`

and `red`

, we advice to refer them as `lastTrafficLightColors.red`

if needed.
Our powerful *SAML* IDE will even remind when you are using ambiguous definitions.
Moreover it will also display if there are any errors.
If you do want to give our IDE a try, you can just download it for free on our Website.

As you can see in all the examples we showed you, there are multiple ways to model the same systems.
Therefore we do invite you to try *SAML* in the editor here or at trysaml.org.
If you want to learn more about *SAML*, follow along to some other tutorials in the next section.

Besides the basics you learned in this tutorial by now, *SAML* is capable of many other things to make developing formal models much easier.
This includes:

- constants
- failure handling
- templates
- formulas
- ...

In future tutorials we will cover some more aspects of *SAML* with new tutorials.
Until then stay tuned and check back for new examples.

If you want to learn more about *SAML*, you are invited to play around here with the RISE4FUN editor.
For even more tutorials visit trysaml.org.

If you want to get in touch with *SAML*, we would like to invite you to our "**V**erification **E**nvironment for **C**ritical **S**ystems". *VECS* was specifically designed to be used in perfect combination with *SAML*.

*VECS* was developed using the popular Eclipse Framework.
Thus *VECS* includes the most necessary features of modern IDEs.
Additionally it comes some with unique features like:

- perfect integration of different
**qualitative**and**quantitative**model checkers - a
**clean**,**well structured**and**graphical**presentation of model checking**results** **fast**,**perfectly integrated**development workflow for your formal models- intuitive and customisable
**syntax highlighting**of formal models - fast
**auto completion**of all elements in*SAML* - expressive
**errors**and**warnings** - intelligent
**quick fixes**for errors and warning - a graphical
**outline**for every model - advanced, easy-to-use
**model management** **1-click model checking**with different model checkers- enhanced model
**debugging** **fast**and**correct transformation**of*SAML*in various model checking languages**consistent results**within various model checkers

If you want to learn more about *VECS* or download *VECS* for free, visit our Website.