ISSN : 1796-217X
Volume : 2    Issue : 3    Date : September 2007

A Tool Support for Design and Validation of Communication Protocol using State Transition
Diagrams and Patterns
YoungJoon Byun
Page(s): 56-63
Full Text:
PDF (402 KB)

In this paper, we introduce a software tool to assist design and validation of a communication
protocol specified in state transition diagrams and patterns. When protocol developers start
development of a new system, they tend to describe the developing system with several highlevel
description elements such as communicating blocks, communication paths, messages, and finite
state machines. Then, they want to validate the correctness of their design as early as possible to
find out any faults in the design. In this paper, we propose a software tool with which protocol
developers can specify structural architectures and behavioral main operations of a protocol system
through the graphical user interface. Then, the tool generates PROMELA code from the design
specification to make it possible for the developers to validate the specification using the SPIN
model checker. Meanwhile, we can specify a protocol system with more high-level abstraction using
a pattern, a combination of several basic elements of the protocol. A pattern is a software reuse
mechanism to apply a well-known solution of a recurring problem to the similar software
developments repeatedly. In the paper, we also propose the usage of patterns in our tool. Using the
pattern support, it will be possible for the tool to provide automatic pattern selection, instantiation,
and composition. As results of this tool, protocol developers can describe a communication
protocol more efficiently and reduce the development cost. Furthermore, they can have the
confidence for the specification at the early stage of software development.

Index Terms
software tool, state transition diagram, communication protocols, SPIN, PROMELA, patterns