Pattern-based design and validation of communication protocols.

摘要

Patterns help to improve software quality and reduce development cost by reusing the experience of experts for recurring problems. In this dissertation, we apply the pattern concept to the development of communication protocols, particularly focusing on the description and validation of message interaction in the protocols. Typically, it is important for designers to capture essential functions of a system at the initial design phase and uncover design errors as early as possible to prevent the errors from affecting later phases. There are many useful patterns for communication systems, but to date they are mainly concentrated on the object-oriented design and implementation. There is little research on the patterns for message interaction and the validation of pattern-based design. We hypothesize that many communication protocols can be developed using a few recurring patterns.;In this pattern-based methodology, we propose a set of patterns to describe the architectural and behavioral specification of communication protocols. A complex protocol can be obtained by composing such patterns. To provide confidence in the design, we suggest a validation method for the design using the SPIN model checker. The validation is composed of model construction for the design and identification of desired properties of the system. Then, the model is checked against the properties. The most difficult part of using tools such as SPIN is obtaining the appropriate properties of a system in a formal way against which to check the design. An innovative feature of our patterns is a section that helps the designer obtain the properties in linear temporal logic.;To show the usefulness of our methodology, we perform several case studies. From the methodology, protocol designers can abstract a system in several patterns and uncover design errors before the detailed design and implementation.