Title
A Tool Support for Design and Validation of Communication Protocol using State Transition Diagrams and Patterns
Abstract
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 high- level 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.
Year
DOI
Venue
2007
10.4304/jsw.2.3.56-63
JSW
Keywords
Field
DocType
index terms—software tool,patterns,communication protocols,spin,promela,state transition diagram,software development,communication protocol,graphic user interface,indexing terms,finite state machine
Programming language,Computer science,Correctness,Finite-state machine,Software,Promela,Design specification,Software development,SPIN model checker,Communications protocol
Journal
Volume
Issue
Citations 
2
3
0
PageRank 
References 
Authors
0.34
3
1
Name
Order
Citations
PageRank
Youngjoon Byun1134.09