Verification Tools for SDL

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.
  

IF: An Intermediate Representation for SDL and its Applications

Experience with Formal Verification of SDL Protocols

• Directly about if2pml:
  • Model Checking SDL with Spin
  • IF: A Validation Environment for Timed Asynchronous Systems
• Related papers:
  • Embedding a Dialect of SDL in PROMELA (TNSDL, a dialect of SDL-88)
  • Extending the Translation from SDL to Promel

• Descrete Time PROMELA and SPIN
• Extending PROMELA and SPIN with Descrete Time

• 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.

• 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. 

• 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.
  
  

• 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
  

• 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).

• 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

• 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