A hybrid approach to design correct communication protocols

Abstract

A protocol is a set of rules which govern the interaction between communicating machines. Protocol analysis and synthesis are two approaches to guarantee that the communication between two machines satisfies progress properties. Although the analysis approach is much easier to design and more flexible than the synthesis approach for general cases, the analysis approach usually suffers the state space problem. Moreover, the analysis approach can be used to detect logical errors in the protocol but not to correct those errors, while the synthesis approach can produce a correct protocol. To make a compromise between these two approaches and have advantage of both approaches, in this paper, we propose an algorithm to design correct protocols by applying both approaches. Given a protocol, we first apply the analysis approach to construct two machines which satisfy certain conditions. Then, we apply the synthesis approach to detect possible errors and provide the designer several choices to correct the errors.

Key words:

• computer networks
• communication protocols
• distributed systems
• protocol synthesis
• protocol validation

Notes

Correspondence addressee