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

Case studies on SDL verification

Please feel free to suggest further tools or submit change requests by email to Eric Bodden or Michael Weber.

Overview

Iulian Ober, Alain Kerbrat (Telelogic), June 2001
Verification of quantitative temporal properties of SDL specifications

Paper
download
Verification goal
Verification of quantitative temporal properties of SDL in order to broaden the class of analyzable specifications and to improve the handling of non-deterministic systems
Example case
SpaceWire (protocol for high-speed data links)
Problems addressed
  • Expressing the semantics of time in SDL in terms of timed automata concepts
  • Employing a user friendly automata-based property specification language (GOAL)
Procedure and restrictions
  • Map the semantics of SDL to that of timed automata
  • restricts SDL designer to use only a limited set of constructs for modeling timing conditions: timers and linear conditions on now
Tooling employed
Temporal property verification tool
  • based on ObjectGEODE
  • supports SDL-96 plus some custom extensions

 TOP

Adekunle, Scheiner, 1999
Detecting Feature Interactions in the Terrestrial Trunked Radio (TETRA) Network using Promela and Xspin

Paper
download
Sourcecode
download full source code of "stage 3" of this paper (internal access only)
Verification goal
Find interactions of (newly intrioduced, additional) network features with other ones (the former set of features)
This work does not use SDL directly! The authors derive rather manually a PROMELA input file from the SDL!
Example case
Terrestrial Trunked Radio (TETRA) (open digital trunked radio standard)
Procedure and restrictions
  • Requirements specification:
    • Construct/extract base requirements by an informal textual description
    • Convert  this description into a temporal formula consisting of propositions and temporal operators (the specification for the model check)
    • Propositions are defined using messages and variables as parameters identified by the information extraction process (first step)
  • Modelling of the system directly in PROMELA
  • Validation of the model using Xspin on the PROMELA input
  • Extraction of feature interactions also through SPIN
Tooling employed
  • SPIN respectively Xspin (GUI for SPIN)

 TOP

Marius Minea, Cornel Izbasa, Calin Jebelean, July 2003
Experience with Formal Verification of SDL Protocols

Paper
download
Verification goal
Test  application of formal methods to the verification of communication protocols.
Example case
One component block of telephone switching software by Alcatel Romania
Problems addressed Test of feasability/scalability of formal verification
Procedure and restrictions
  • standard SDL -> IF -> C code conversion
  • restrictions are basically those of the sdl2if converter
Tooling employed
  • IF toolset by Verimag:
    • sdl2if (SDL to IF conversion)
    • if2if (translations on IF)
  • if.open compiler (compiles IF into C sources which can be used for state space exploration and simulation)

 TOP

Guoping Jia, Susanne Graf, 2001
Verification experiments on the MASCARA protocol

Paper
download
Verification goal
Apply verification to a real protocol in order to test feasabilityof verification for reasonably large projects
Example case
ATM protocol MASCARA
Problems addressed
  • Open questions, partially solved:
    • How to extract a subsystem from a large SDL specification?
    • How to get reasonable abstraction of the neglected parts of the system?
    • How to get requirements?
    • How to express properties?
    • How to analyze negative verification results?
    • How far can we go with system verification?
Procedure and restrictions
  • Optimization techniques:
    • Partial order reduction
    • Atomicity reduction
    • On-the-fly model checking
  • Compositional verification
Tooling employed

 TOP

Ursula Hinkel, 1998
Verification of SDL Specifications on the Basis of Stream Semantics

Paper
download
Verification goal
First feasability study of SDL verification in general
Example case
Alternating Bit Protocol
Problems addressed
  • stream semantics
  • higher order logic
  • domain theory
Procedure and restrictions
Tooling employed


 TOP

Misc papers about this topic

 TOP
Valid HTML 4.01 Strict! Valid CSS!