A Tool Support for Design and Validation of Communication Protocol using State Transition Diagrams

In this paper, we introduce a software tool to assist design and validation of a communication protocol specified in state transition diagrams. 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 and behavioral key functionalities of a protocol system through the graphical user interface. Then, the tool generates PROMELA code from the design specification to make it possible for developers to validate the specification using the SPIN model checker. As results of this tool, developers can describe a communication protocol more efficiently and have the confidence for the specification at the early stage of software development