Specification and Validation of Communications in Client/Server Models

Errors such as deadlock and race condition are very common yet extremely difficult to debug in the communications design of client/server models based on remote procedure call and multi-threading. This paper presents an effective approach to detect these errors. It shows how to apply the specification and validation techniques in Protocol Engineering to discover those errors in the early stage 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 then is built to convert PROMELA-C/S to PROMELA for running validation using SPIN. The paper also reports the results of some specification and validation trials using PROMELA-C/S, its translator, and SPIN