Abstract:

In this paper we use a probabilistic-timed version of Lotos (PTLotos) for specifying and verifying the Alternating Bit Protocol (ABP). First, we present the language which is an upward compatible version of Lotos where some new operators to deal with time and probabilistic features have been included. We give an operational semantics, where there are two kinds of transitions: probabilistic transitions and timed transitions. Transitions of the first kind are associated with the events that a behavior expression can execute, while timed transitions deal with time evolution. From this operational semantics we define a testing semantics, where a process passes a test with a probability in a period of time, and two processes are intended to be equivalent if they pass all the tests with the same probability for any time.

In the second part of the paper, we use PTLotos in order to specify the Alternating Bit Protocol. The ABP is a simple communication protocol which provides an error free communication over a faulty medium. The protocol has three components: the sender, the receiver and the (faulty) medium, where we suppose that the medium may lose the messages. The only observable events of the whole system will be mess (indicating that a message has been sent) and deli (indicating that a message has been received and delivered). Once we have specified the three components and we have described the whole system, we verify that our specification fulfills some good properties. Because of the testing semantics we have defined, we can make assumptions about the environment, and we can express them using tests, and so, we can get information about the behavior of the protocol by studying the interaction between such tests and the specification of the ABP.