Bisimulation analysis of SDL-expressed protocols: a case study
Marsha Chećhik, Hai Wang · 2000
This paper presents a family of new protocols, termed Asynchronous Retransmission Go-Back-N (AR), which are improvements on the Go-Back-N protocol in environments characterized by high error rates and/or large propagation delays. In order to verify that the use of these protocols, expressed in SDL, is transparent to the user, we explore the feasibility of their bisimulation checking. We discuss the main issues involved in translating SDL into Concurrency Workbench, a tool for performing bisimulation checking, and apply the results to verifying correctness of AR protocols. Keywords: Network protocols, SDL, Concurrency Workbench, Go-Back-N protocol, bisimulation. 1. Introduction As computer-communication systems become more complex, it is becoming more and more important to ensure the correctness of protocols they rely on. In addition, faster, better algorithms are often discovered, and it is desirable to be able to replace the old algorithm by a new in a manner that is completely tr...