[I2 logo] [RWTH logo] MOVES: Software Modeling and Verification
(Informatik 2)
Computer Science / RWTH / I2 / Research / AG / MCS / SDL
Printer-friendly

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.
IF toolset
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

imPROVE-SDL

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.

UPPAAL

Purpose Graphical (T)CTL model checker (fragment of TCTL, where quantification may only appear at the beginning of a formula)
SDL Input SDL/PR
Internal representation
XTA
Converstion / Prerequisites
SDL/PR -> [sdl2xta] -> XTA
Papers
Timing analysis of an SDL subset in UPPAAL (Hessel)
Presentations
ARTES, ASTEC
Additional strengths
Express time consumption for constructs in SDL_XTA processes.

TOP

KRONOS

Purpose (T)CTL model checker
SDL Input SDL/PR
Internal representation
IF
Prerequisites
SDL/PR -> [sdl2if] -> IF
Presentation slides about KRONOS and SDL
here
Papers about KRONOS and SDL

IF: An Intermediate Representation for SDL and its Applications

Experience with Formal Verification of SDL Protocols

SDL support
see SDL2IF

TOP

SPIN

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
SDL support
see SDL2IF and IF2PML

TOP

DTSPIN

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

PSPIN (distributed SPIN)

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

CADP

SDL Input SDL/PR
Internal representation
LOTOS
Employed conversion
SDL/PR -> [sdl2if] -> IF
Papers various
SDL support
only certain tools of the CADP toolset can read IF, such are: ALDEBARAN and EVALUATOR (see this paper, page 125)
see SDL2IF

TOP

Converters

SDL2XTA

Evaluation of SDL2XTA (internal)

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

SDL2IF

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

IF2PML

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
Valid HTML 4.01 Strict! Valid CSS!