This directory contains files for Technical Report CSRI-382.

The files in this directory are the following:

1) README       (< 1   KB - the ASCII file you are now reading)
2) TR-382.ps    (313.5 KB - PostScript)
3) TR-382.ps.gz (83    KB - PostScript compressed with the program "gzip")

If you have the UNIX "gunzip" program, get the file TR-382.ps.gz.
Remember to transfer the file in binary mode. After the transfer, 
"gunzip" the file.

If you do not have the UNIX "gunzip" program, get the file TR-382.ps 
in ASCII mode. 

After transfering the file, print it on a PostScript printer.

If you have any questions or comments about this technical report, please
contact chechik@cs.toronto.edu


TITLE:    Feasibility of Bisimulation Analysis of Protocols
          Expressed in SDL: A Case Study
AUTHORS:  Marsha Chechik and Hai Wang


ABSTRACT:

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.