Feasibility of Bisimulation Analysis of Protocols Expressed in SDL: A Case Study


Faster, better networks algorithms are often being discovered, and it is desirable to be able to replace an old algorithm by a new in a manner that is completely transparent to the application using it. This paper investigates the technique for ensuring such transparency for protocols expressed in SDL, via bisimulation checking. We discuss the main issues involved in translating SDL into Concurrency Workbench, a tool for performing bisimulation checking, and illustrate the feasibility of the technique by comparing the SDL specification of the Go-BackN protocol with the family of new protocols, called Asynchronous Retransmission Go-Back-N (AR). The latter perform better in environments characterized by high error rates and/or large propagation delays.