Spin Model Checker GUI manual

From TASTE
Jump to: navigation, search

Overview

The purpose of this manual is to provide the user an introduction to formal model verification in TASTE. The formal model verification is an approach to model validation, in which all possible states of the model are explored automatically and during the exploration, the requirements are verified. The requirements for the model are created by the user using few available methods.

The user shall be familiar with the TASTE, in particular SDL and ASN.1. At this moment the SDL is only one method which allows to define the behaviour of the model, therefore this section describes the semantic of Interface View and behaviour of Functions implemented in SDL.

The main part of TASTE Project is an Interface View, in which the logical structure of the project is defined. The Interface View consists of a set of Functions, which are connected via interfaces. Additionally, the Function can be instance of Function Type. Additionally, every SDL function has an mutex or interface to protect its internal state, which can be shared between few threads. Every interface is a declaration how the functions can exchange messages. The supported kinds of interfaces in Spin Model Checker are:

  • Sporadic – where the communication is asynchronous, i.e. caller continues execution even if the message is not handled by callee. Sporadic interface can have at most one parameter.
  • Protected – where the communication is synchronous, i.e. caller cannot continue execution if message is not handled by callee. Protected interface can have many parameters, they can be used as output or input to exchange data between functions in both directions.
  • Unprotected – same as protected, except that they do not lock the function semaphore.

The remaining kind of interface – cyclic – is not supported by Spin Model Checker.

Moreover, the sporadic interfaces are implemented as threads, every thread has an infinite loop in which waits for the incoming messages on queue. After reception of a message, the thread locks the function mutex and executes code which handles the message. After this, the lock is released and the thread continues waiting. Every aforementioned queue has a size property, which is equal to 1 by default. Also, every sporadic interface has a priority.

The semantic of TASTE project described above was baseline for an approach how the model is translated into Promela, the language used for formal verification. The translation mimics the structure of executable files created by TASTE as close as possible. So the model under verification consists of a set of proctypes (threads), channels and locks.

All the functions, which are not implemented in SDL (like GUI, C or Ada) are mapped into Environment Functions, another crucial topic from the perspective of Spin Model Checker. The Environment Function is an entity which provides test vectors and stimulation for the model.

For the provided sporadic interfaces in Environment Functions there is corresponding proctype (thread), which generates messages in loop, and puts them into the queue. For every required protected and unprotected interface, there’s a Promela Code, which generates values for Output parameters.

The ASN.1 in TASTE is responsible for Data View. The user can define complex data types, which can be used to specify the types of parameters in interfaces or internally in SDL processes. The ASN.1 allows to define constrains for values, e.g. available ranges of integer datatypes or sizes of the arrays. The Spin Model Checker supports the validation of specified constraints during verification process. In case, when the behaviour of the model can lead to violation of constraints from Data View, the Spin Model Checker reports this as an issue.

Running Spin Model Checker

The main part of Spin Model Checker GUI, the Model Checking Window is available from Interface View editor, as presented on image below. To open the window the user shall click on marked item.

Interface View editor

The Model Checking Window is divided into four tabs. The first tab – Configuration – is common for Simulator and IF Model Checker. The Spin Model Checker tab is presented on the image below. The user shall switch to the marked tab to proceed.

Model Checking Window

If the Interface View of the project is prepared, i.e. it is non empty, all the interfaces are connected and all the SDL Functions are implemented the user can directly click the Call Spin button as presented on image above.

After that the new dialog window shall appear, which allows the user to select the output directory for intermediate files and reports for the verification process. The selected directory shall be different than root directory of the project. The best approach is to create a new directory. After this user will be warned that the content of the selected directory will be removed, it is the last chance to cancel the verification process. If the user agrees to continue, a new window shall appear. It is similar to text console and it contains the text with detailed description of steps of verification process. After the process finishes, the window should show FINISHED at the end of text.

Spin Model Checker output

The next important element of the verification is the report in HTML format, which automatically appears in the browser after end of the verification process.

Spin Model Checker report

The HTML file is located in the output directory selected by user after click on Call Spin button. The directory contains also generated Simulator Trails for every found error.

Configuration

The configuration tab contains three areas, which are used to specify the properties, functions and subtypes for the model.


Configuration

Properties

Stop Conditions

The Stop Conditions is the textual format, which allows to specify Boolean expressions which will be evaluated constantly during the process of verification. To create a new file the use shall right click on properties and select New property menu item. In the next dialog window the user shall select Boolean Stop Condition – LTL from Combo Box and click Ok. In the next dialog the user shall specify the name of the file. After clicking Ok again, the empty file will be available as presented below.

Adding Stop Condition

The user can double click on newly created item to edit it inside Space Creator. The example, which presents the syntax highlighting feature, is presented below.

Example Stop Condition

Observers

The observers is a method of expressing requirements for model using state machine in SDL. The observers have ability to observe and modify signals, check and change state of processes in model and also detect signal loss. To create the new observer, the user should right click on properties and select New property menu item. In the next dialog window the user shall select Observer from Combo Box and click Ok. In the next dialog the user shall specify the name of the file. After clocking Ok again, the newly created file will be available as presented below.

Adding Observer

The user can double click on newly created item to edit it inside OpenGEODE. The first step is to remove declaration of observe procedure and add observer signals using 'renames'. The two next images present newly created observer and the observer with defined signals.

New Observer
Definition of signals in observer

MSCs

The MSCs are experimenting format for specifying desired and unwanted message exchanges between processes. The semantic of MSC specified in Spin Model Checker allows to translate it into Observer, which is state machine. To create the new MSC property, the user shall right clock on properties and select new property menu item. In the next dialog window the user shall select Message Sequence Chart – When/Then and click Ok. In the next dialog the user shall specify the name of the file. After clicking Ok again, the newly created file will be available as presented below.

Adding MSC

The user can double click on newly created item to edit it inside Space Creator. The example is presented on image below.

Example MSC

Selecting functions

Using the list From the Select functions (submodel) the user is able to specify which functions shall be part of the model under verification. By default are functions from Interface View are included. The functions excluded by the user, together with their interfaces won’t be included into model under verification.

Subtyping for environment's interfaces

The area Select environment subtypes contains a list of selectable asn files. The widget allows to select at most one subtype file. If the file with name empty.asn is visible on the list, it shouldn’t be selected by the user. The purpose of this file is to ensure compatibility between existing model checker engines. To create a new subtype asn file the user shall right click on the subtypes folder and select the New subtypes menu item. In the dialog window the user shall specify the name of the file and click OK. After clicking Ok again, the newly created file will be available as presented below.

Adding subtype

The user can double click on newly created item to edit it inside Space Creator. The example is presented on image below.

Example subtypw definition

This image presents a subtype for one specific example. The Interface View is presented below.

Example Interface View

The Function ModeManager is a function implemented in SDL while Sensor and EGSE are implemented in GUI, what makes them part of environment. The Sensor function has only one required interface with name reading. This interface has a parameter with name X and type defined in ASN:

  TInteger ::= INTEGER (0 .. 1000000)

The EGSE function has required interface with name tc and parameter cfg. The type of parameter is defined in ASN as:

  TConfig ::= SEQUENCE {
      param-a TInteger,
      param-b TInteger
  }

The allowed values for both parameters makes unfeasible process of verification. To change the allowed values, first the limited of only few allowed values is defined as Small-Integer. To specify the type for particular interface, the type with following name can be declared by user.

  <function>-<interface>-<parameter>

Where every character is lowercase except first, like every ASN.1 type name.

As shown on example above, the file defines new parameters for two environment interfaces. The first one, Egse-tc-cfg, is required interface in Egse function, while the second is required interface in the Sensor function. The Spin Model Checker allows to define subtypes for sporadic interfaces and for OUT parameters in protected/unprotected interfaces.

Options

Spin options

The tab SPIN model-checker in Model Checking Window provides a set of customizable options:

  • Use bit hashing – enables bitstate mode,
  • Search shortest path – In case of error, the shortest path leading to the error is produced, this option limits number of errors to 1,
  • Use fair scheduling – enables weak fairness in scheduling the order of execution for concurrent processes,
  • Support ASN.1 REAL – Enables support for REAL datatype (this requires modified version of Spin),
  • Number of cores – Number of working threads (default 1),
  • Time limit (sec) for exploration – Time limit for execution in seconds (default 300),
  • Exploration mode – Two available options: Depth First Search and Breadth first search are described in next section,
  • Search state limit – The maximum number of states in execution path (default 1000000),
  • Error limit – Limit of the numbers of errors, after the verifier stops state exploration,
  • Memory limit [MB] – The upper limit of memory that can be allocated by verifier process,
  • Global input vector generation limit – Maximum number of messages send by environment during verification,
  • Delta value for ASN.1 REAL value generation – Described in separate section,
  • VECTORSZ value – The limit for state vector size,
  • Interface generation limits – The limit for number of generated messages for specific interface from environment.

The default exploration mode in Spin Model Checker is Depth First Search. In this mode the verifier explores possible states continuously, so if error was found, it is not guaranted that the scenartio is shortest, nevertheless it is possible to this mode together with option Search shortest path. The other exploration mode, Breadth First Search, switches the verifier to explore shortests scenarios from the beginning. The limitation of Breadth First Search is that it cannot be used to detect acceptance cycles, i.e. eventually clauses from Stop Conditions and Success States from observers.

The original version of spin does not support floating point data type. Few approaches were considered how to support REAL datatype from ASN.1 in TASTE Spin Model Checker. The selected solution was to fork Spin and add support to floating point type. The source code is available on github. The change of the spin executable used in verification process, the user shall change the global settings.

The detailed descriptions of parameters for spin and verifier is available at [[1]] and [[2]].

Loading and saving configuration

The user has an ability to save the model checker configuration and later load it. The configuration preserves all options from Model Checking Window – Configuration, SPIN model-checker and options from two remaining tabs.

To save the configuration the user shall click the button Load configuration located on the bottom of Model Checking Window. In the next dialog window the user shall select the destination directory and the name of the XML file.

The destination directory shall be different from output directory used by Spin Model Checker.

To load the configuration the user shall click the button Load Configuration and in the next dialog window select the XML file to load.

Settings

The Spin Model Checker provides user interface to configure global settings. It is available from main Space Creator window via Menubar. To open the settings the user shall select Edit->Preferences…

In the new window the user shall select SpaceCreator from the left pane and later tab Taste Model Checker settings as shown on image below.

Spin Model Checker settings

The two customizable options are provided:

  • Spin executable – a path or command to the spin executable
  • Default output directory (relative to project root) – the default directory for intermediate files used in verification process.

Results

When the errors are found by model checker, the report contains description of eac error and also simulator trace with scenario how the state was reached. The example report is presented below.

Example report with error

The types of possible errors are:

  • stop condition violation - the report contains the text of violated stop condition,
  • range assertion - the report contains the name of variable,
  • observer error state - the name of the observer is shown,
  • MSC violation - the name of the MSC is shown.

Simulator traces

For every found error, the Spin Model Checker produces a Simlator Trail with scenario. The simulator trail is a text file with extension .sim, which contains the sequence of events in ASN.1 Value Notation format. The list of produced traces is visible in Model Checking Window, together with the generated HTML report. The user can double click on items to open them in the browser or system default text editor.

Example list of produced files

Troubleshooting

In case of the problem, i.e. when Verifier is not able to run verification, the first step, to debug shall be to clean the project using make clean from commandline, and then open and save all SDL files and try again.

This is due to the fact that OpenGEODE generates ASN.1 datamodel of the process only during save, therefore the user shall do this manually for every SDL function in the Interface View.

In case when observers are present (they are also edited in OpenGEODE), the regeneration is more complicated. After aforementioned step, the user shall run the verification process and if it ends with an verifier error, then the user shall close Space Creator and run the following command in the project root directory:

   src=`find work/simulation -name 'observer.asn' -type f`; for dst in `find work/modelchecking -name observer.asn`; do cp -v "$src" "$dst"; done;

as presented on image below:

Project regeneration

After this the user shall open project in Space Creator again, then open and save all SDL files which belongs to observers. This should solve most of the common issues.

Another important advice is to always make sure that the queue sizes connected to environment functions have the size property equal to 1.

Before reporting a potential bug, the user should try to reproduce it on the latest version available of TASTE. This simplest way is to Update TASTE using script.