Title :
Specification and validation of communications in client/server models
Author_Institution :
Bellcore, Morristown, NJ, USA
Abstract :
Errors such as deadlock and race conditions are very common yet extremely difficult to debug in the communications design of client/server models based on remote procedure calls and multi-threading. This paper presents an effective approach to detecting these errors. It shows how to apply the specification and validation techniques used in protocol engineering to discover those errors in the early stages of a client/server software development. The work is based on the protocol specification and validation tool PROMELA/SPIN. PROMELA is extended to a new language called PROMELA-C/S for additional expressive power of specifying client/server communications. A PROMELA-C/S translator is built to convert PROMELA-C/S to PROMELA for validation using SPIN. The paper also reports the results of some specification and validation trials using PROMELA-C/S, its translator, and SPIN
Keywords :
client-server systems; fault diagnosis; hazards and race conditions; program debugging; program interpreters; protocols; queueing theory; remote procedure calls; software tools; specification languages; PROMELA-C/S language; PROMELA/SPIN; client/server models; client/server software development; communications design; communications error detection; deadlock; debugging; distributed systems; multi-threading; protocol engineering; protocol specification; protocol validation; race conditions; remote procedure calls; translator; Data structures; Debugging; Message passing; Power engineering and energy; Power system modeling; Process design; Programming; Protocols; System recovery; Yarn;
Conference_Titel :
Network Protocols, 1994. Proceedings., 1994 International Conference on
Conference_Location :
Boston, MA
Print_ISBN :
0-8186-6685-4
DOI :
10.1109/ICNP.1994.344370
