SAML - tutorial

Getting started with SAML

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!

Introduction

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.

Components

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.

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:

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.

Model checking

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 NUSMVSPECs or PRISMSPECs. 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.

NUSMV specifications

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:

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

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

PRISM specifications

If you want to use a quantitative model checker like PRISM you have to use PRISMSPEC. Like 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 =, <, <=, >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.

Enumerations

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.

Extending the traffic lights

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?

An additional enumeration item

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.

An additional state variable

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.

Minimizing the effort

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.

Other tutorials

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.

The SAML IDE: VECS

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.

Contact Us| Privacy & Cookies | Terms of Use | Trademarks| © 2021 Microsoft