SAML (System Analysis Modelling Language) 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
10 and is initialized with
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
The first update rule specifies that if the current value of
0, the following value will be also
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
The last update rule specifies the same behavior as the first rule, thus if the value of
10, it will remain at
If you do specify update rules in SAML, you do have to keep some important aspects in mind:
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
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
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 Computation Tree Logic expressions. Thus they are specified trough the following syntax:
expression) - [not] exists globally
expression) - [not] exists next state
expression) - [not] exists finally
expression) - [not] for all globally
expression) - [not] for all next state
expression) - [not] for all finally
expression) - [not] exists until
expression) - [not] for all until
expressions can contain other CTL expressions or simple logical expressions using the following logical elements:
If you want to use a quantitative model checker like PRISM you have to use
NUSMVSPECs they are specified trough the following syntax:
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
x operator has to be replaced with a probability ranging from
PRISM will then compute, if the probability is within that bound.
In addition to
P it is possible to specify
Pmax in combination with
In that case, PRISM will compute the minimum and respectively maximum probability of the occurce of the given
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
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.
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
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
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
Hence we do have an ambiguous definition of the enum values
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:
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 "Verification Environment for Critical Systems". 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:
If you want to learn more about VECS or download VECS for free, visit our Website.