Rules for synthesizing correct communication protocols

ABSTRACT

An approach to communication protocols synthesis is proposed which permits the development of general (FIFO and non-FIFO channels), N-party (N>=2) protocols with the following properties: completeness, deadlock freeness, livelock or tempo-blocking freeness, termination or cyclic behavior, liveness, boundedness and absence of non-executable interactions.

REFERENCES

• 1: {Berthomieu80}, Berthomieu, B., "Proving Progress Properties of Communication Protocols in Affirm," USC-ISI MEMO-35-BB, October 16, 1980.
• 2: {Bochmann77}, Bochmann, G. V., and Gecsei, J., "A Unified Method for the Specification and Verification of Protocols," Proc. IFIP Cong., 1977.
• 3: {Bochmann78}, Bochmann, G. V., "Finite State Description of Communication Protocols," Comp. Networks, Vol. 2, pp. 361--372, 1978.
• 4: {Brand80}, Brand, D., and Zafiropulo, P., "Synthesis of Protocols for Unlimited Number of Processes," Proc. Trends and Application: 1980 Computer Network Protocols, NBS, Gaitherberg, MD, 1980.
• 5: {Devy79}, Devy, M., and Diaz, M., "Multilevel Specification and Validation of the Control in Communication Systems," Proc. Ist Distr. Comp. Systs., Hunsville, Alabama, (October 1979).
• 6: {Gouda81}, Gouda, M. G., and Yu, Y. T., "Designing Deadlock-Free and Bounded Communication Protocols," University of Texas, Austin, TX Report TR-179, (June 1981).
• 7: {Hailpern80}, Hailpern, B., and Owicki, S., "Verifying Network Protocol Using Temporal Logic," Proc. Trends and Application: 1980 Computer Network Protocols, NBS, Gaitherberg, MD, 1980.
• 8: {Harangozo78}, Harangozo, J., "Protocol Definition with Formal Grammers," Proc. Symp. on Computer Comm. Protocols, Liege, Belgium, 1978.
• 9: {Merlin79}, Merlin, P. M., "Specification and Verification of Protocols," IEEE Trans. Comm COM-27, No. 11, (June 1979).
• 10: {Merlin80}, Merlin, P. M., and Bochmann, G. V., "On the Construction of Communication Protocols and Module Specification," to appear in ACM TOPLAS (1981).
• 11: {Owicki80}, Owicki, S., and Lamport, L., "Proving Liveness Properties of Concurrent Programs," Stanford University Report, (October 14, 1980).
• 12: Jonathan Bruce Postel, A graph-model analysis of computer communications protocols., 1974
• 13: {Razouk80}, Razouk, R. R., and Estrin, G., "Validation of the X.21 Interface Specification Using SARA," Proc. Trends and Application: 1980 Computer Network Protocols, NBS, Gaitherberg, MD, 1980.
• 14: {Schwartz81}, Schwartz, R. L., and Melliar-Smith, P. M., "Temporal Logic Specification of Distributed Systems," Proc. Second Int. Conf. on Dist. Systs., Paris, France, (April 8--10, 1981).
• 15: {Sidhu80}, Sidhu, D. P., "General Approach to Protocol Synthesis and Analysis: I," BNL Preprint (1980), to be submitted for publication.
• 16: D P Sidhu, Authentication protocols for computer networks: I, Computer Networks and ISDN Systems, v.11 n.4, p.297-310, April 1986 [doi>10.1016/0169-7552(86)90004-8]
• 17: {Sidhu81}, Sidhu, D. P., "Toward Constructing Verifiable Communication Protocols," in Proc. of Protocol Testing - Towards Proof?, INWG/NPL Workshop, National Physical Laboratory, Teddington, U.K., (27--29 May 1981).
• 18: {Sunshine75}, Sunshine, C. A., "Interprocess Communication Protocols for Computer Networks," Tech. Report No. 105 Digital Systems Lab. Standard University, CA, 1975.
• 19: {Sunshine79}, Sunshine, C. A., "Formal Methods for Communication Protocol Specification Verification, A Rand Note, N-1429-ARPA/NBS, Nov. 1979.
• 20: {Thompson81}, Thompson, D., et al., "Specification and Verification of Communication Protocols in AFFIRM Using State Transition Models," USC-ISI Report 81-88, March 1981.
• 21: {West78}, West, C. H., "General Technique for Communications Protocol Validation," IBM J. Res. Develop., Vol. 22, pp. 393--404, July 1978.
• 22: {Zafiropulo80}, Zafiropulo, P., "Towards Analyzing and Synthesizing Protocols," IEEE Trans. Comm, COM-28, No. 4, (April 1980).