|
MOVES: Software Modeling and Verification
(Informatik 2)
|
Verification
Tools for SDL
Please feel
free to suggest further tools or submit change requests by email to Eric Bodden or Michael Weber.
Tools and frameworks for SDL processing
For tooling have a look here.
Case studies on SDL verification
For case studies have a look here.
Overview
General Terms
IF
|
Internal Format - an
intermediate representation used as input for KRONOS, SPIN (via PROMELA)
and so on. The IF
toolset provides tooling aroung IF.

|
SDL
|
Specification and Description
Language as defined through the ITU Z.100
recommendation
|
SDL/PR
|
Phrase representation of SDL;
can be mapped to SDL/GR (graphical representation) and vice versa
|
TOP
General SDL Tools
The SDL forum gives an
overview on available tools for SDL.
TOP
Verification Tools
with SDL support
Purpose |
Verification tool specialized on
SDL |
SDL support
|
SDL92/96 input directly supported |
Additional strengths
|
Vendor's statement:
- Easily interfaced to any commercial SDL Editor tool
- Automatic; no mathematical knowledge necessary
- Quick enough for interactive debugging (typical runs in a
few minutes)
- Used for exhaustive debugging, coverage enhancement,
functional performance analysis, proofs of properties, specification
clarification
- Properties specified in SDL or MSC
- GUI and scripted interfaces for convenience
- imPROVE-SDL operates on Windows, Sun Solaris and Linux.
|
TOP
TOP
Purpose |
LTL model checker
|
SDL Input |
SDL/PR
|
Internal representation
|
PROMELA (PROcess MEta LAnguage,
discrete subset of PROMELA); query language: Next-Time free LTL |
Prerequisites
|
SDL/PR
-> [sdl2if] -> IF -> [if2pml]
-> PROMELA |
Papers about SPIN/PROMELA and SDL |
- Directly about if2pml:
- Related papers:
|
SDL support
|
see SDL2IF
and IF2PML |
TOP
Purpose |
Enhanced SPIN for descrete time
(decreasing counters with set
and delay) |
SDL Input |
see above |
Internal representation
|
DT PROMELA (Discrete Time
PROcess MEta LAnguage, discrete subset of PROMELA):
Note that DTSPIN provides no
enhancement to the query language LTL (i.e. no Timed LTL). However it
does provide timers which can be set to a positive value and which can
expire (value 0). Expectations regarding those timers can be modelled
via assertions on the timers' values. The actual decrease of timers can
be implemented entirely in PROMELA (see Extending
PROMELA and SPIN with Descrete Time). Thus DTSPIN provides actually
not really a language enhancement but rather an automatec include of a timer data type and some macro
based operation on this type. |
Prerequisites
|
see above |
Papers about DTSPIN |
|
SDL support
|
no direct support, probably seeabove |
TOP
Purpose |
Parallel SPIN implementation |
SDL Input |
see
above |
Internal representation
|
see
above |
Prerequisites
|
see
above |
Papers about DTSPIN |
- Distributed
Model Checking with SPIN
The authors present an implementation of SPIN that is able to share the
state space between various workstations over TCP/IP. The major
scientific contribution of this paper is a partitioning algorithm that
tries to distribute the state space over the workstations in such a way
that communication is minimized. During this partitioning, usual SPIN
mimimization efforts like e.g. partial order reduction are preserved.
|
SDL support
|
no direct support, probably see
above |
TOP
TOP
Converters
Purpose
|
conversion of SDL/PR
to XTA
(input for UPPAAL) |
Distribution
|
avaliable on the author's website
available as freeware Linux binary only
|
Technology
|
see paper Timing analysis of an SDL subset
in UPPAAL (Hessel) |
Supported versions of UPPAAL
|
by the author:
- Sdl2xta converts into the .xta format, not the .xml format.
It was tested with uppaal 3.2.X And might have get obsolete with
the language "improvement" in 3.4.X There is some conversion tools but I
havn't tested this.
- Answer in a nutshell: 3.2 (.xta) should work for earlier
versions handling .xta formats with templates.
|
SDL support
|
- based on SDL-92
- Uncertain implicit output
- No signal parameters (integers instead)
- No priority inputs
- No continuous signals
- No enabling conditions
- "In this work we have described how it is possible to
convert an SDL syntax to UPPAAL preserving the characteristics of the
environment an SDL process works in." (Hessel Paper, see page 68 for
details)
- by the author:
- Supported: value passing, dynamic processes (up to a max
value) and underspecified signal paths are supported (all
interpretations verified).
- Missing: Procedure calls, and abstract data types. Macro
procedure calls can be done, unless recursive, in one man month. The
value passing is because of limitations in UPPAAL. So integer
representation have to do. The modeller is responsible to transfer the
concepts to integer representation.
|
TOP
Purpose
|
converts SDL/PR
to IF |
Distribution
|
part of the IF (Internal Format)
toolkit, being developed by Verimag
currently available as freeware binary, only for Solaris |
Technology
|
parser based on commercial API
by Telelogic (ObjectGeode)
to run sdl2if a license file for the API mentioned above is required
|
Conversion
|
- SDL structure is flattened (references are inlined)
- structured communication (channels, signal routes,
connection points) is transformed to point to point communication
- all SDL predefined data types are fully converted
- abstract data types: only signatures are translated; user
must provide an appropriate implementation
- implicit pid
parameter of SDLsignals is translated to an explicit one (also sender, offspring, parent)
- SDL states are translated to stable IF states as well as
auxiliarz non stable helper states (save/discard sets are translated 1:1)
- transistions are translated as minimal paths, being eager by default
|
SDL support
|
(info by Marius Bozga, one of
the SDL2IF developers)
- ObjectGEODE compiler is able to pre-process SDL
specifications up to SDL-96 and to transform them, into a kind of
SDL-88. Basically, it can flat the SDL structure by instantianting
"types" (i.e, block types, process types), inheritance and other high
level sonstructs.
- sdl2if takes only this pre-processed version and translates
the most of it
- The parts which are not handled concern mainly
- data types (which can be arbitrarily complex, including
abstract ones, etc...)
- services (they can be handled theoretically with IF, but
we did not encounter them in examples, hence we did not push on this
direction)
- recursive procedures (same reason, for now we handle
procedures by inlining, etc)
- All the rest is handled successfully (process creation,
communication, timing, standard types (including records and arrays,
strings), etc).
- Some papers about
the translation from SDL and IF exists on the IF web site. They
are a bit obsolete because they
relate the translation of SDL into IF-1 (the 1st version of IF), and not
into IF-2 (current version, improved to handle in addition dynamical
aspects of SDL).
|
Paper
|
IF: An
Intermediate Representation for SDL and its Applications
|
TOP
Purpose
|
converts IF to PROMELA
(input format for (DT)SPIN) |
Distribution
|
on the
author's website
currently available as freeware binary, only for Solaris |
SDL support
|
- Save operations are not implemented by if2pml. The tool
generates a warning in such a case. (The paper
above tries to overcome this issue.)
- Enabling conditions (Note: these are not allowed in SDL):
sdl2if only translates them if the conditions do not involve parameters
of the input signal (the user may choose between "saving'' and
"blocking'' semantics). if2pml does not translate enabling conditions.
Note: the "simple'' case where the conditions do not involve parameters
of the input signal can probably be easily handled though.
- ANY (the operation that is absent in SDL, but it is a part
of IF, so these remarks refer to if2pml): ANY on the receiver's side is
translated into _ (an underscore) in Promela. This is semantically
correct.
ANY on the sender's side is translated into 0 (zero). That is not
always correct. It is the user's responsibility to check it
|
Conversion
|
- discard mechanism of SDL is realized via self-looping to
the same state
- atomicity of SDL transitions is preserved by surrounding
theIF statements by an atomic{...}
statement
- omissions: dynamic creation of processes (always maximal
number is created at the start by sdl2if), save statement
- this paper gives an idea about how
the save statement could be
implemented
|
Paper
|
Model
checking SDL with SPIN
|
General papers
TOP
|