MOVES: Software Modeling and Verification
(Informatik 2)

Prof. Dr. Ir. Joost-Pieter Katoen

Computer Science / RWTH / I2 / Research / 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

Misc papers about this topic

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	IF toolset by Verimag: sdl2if (SDL to IF conversion) if2if (translations on IF) CADP

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

[Mail]

Disclaimer

Last modified: 2004-04-28 13:22 UTC