Formalisms and Tools for Design and Specification of Network Protocols
May 2007, 33 pages.
Available as Postscript,
Message Sequence Charts (MSC) are a useful formalism for formalization of
network protocols early in their design phase. In this paper, we introduce
the basics of MSC language and describe some of the possibilities for
automatic location of "problematic" parts in the design. Focus is then given
to different modifications of MSC design (FIFO behavior, bounded channels,
etc. ) as well as formal checking of more complex design properties (MSC
membership, realizability). Next, an introduction of Specification and
Description Language (SDL) is presented. Possibilities of automatic
synthesis of system design in MSC to an SDL model and it`s correctness
verification are mentioned.