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

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.