[ Home | What's New | Contents | Overview | Contributors | Distribution | Examples | Documentation | Manual | Publications | Mailing List Archive | Problems ] This page was last updated by Axel Belinfante on 2003-02-20
TorX Test Tool Information
Prev   Next

Conference Protocol Formal Specifications

This section describes the aspects that are involved in the construction of formal specifications of the conference protocol behaviour in four languages: LOTOS, Promela and SDL. Also the source of the conference protocol specification can be obtained here of all four languages.

LOTOS

The core of the specification is the (state-oriented) description of the conference protocol behaviour, which closely follows the rules sketched in section Protocol behaviour. The CPE behaviour is parameterized with the set of potential conference partners and its CSAP and USAP addresses, and is constrained by the local behaviour at CSAP and USAP. The instantiation of the CPE with concrete values for these parameters is part of the specification.

The CPE interacts with its environment via two output queues: one for data indications to the user, and the other for multicast, broadcast, or point-to-point messages to peer conference partners. These queues are processed in parallel with the processing of incoming service primitives and PDUs; multicast and broadcast messages are offered to the underlying UDP service in all possible interleavings.

The LOTOS SUT specification is available in two variants: One for processing with the LITE LOTOS tool environment, and one for use with the Caesar/Aldebaran Development Package.

The LOTOS conference protocol IUT specification can be obtained here!
The LOTOS conference protocol SUT specification can be obtained here (LITE, library mod-is)!
The LOTOS conference protocol SUT specification can be obtained here (CADP97b)!
The LOTOS conference protocol SUT specification can be obtained here (CADP99d)!

Promela

Communication between conference partners has been modelled by a set of processes, for each potential receiver one, to `allow' all possible interleavings between the several sending of multicasted PDUs. Instantiating the specification with 3 potential conference users, a Promela model for testing is generated which consists of 122 states and 5 processes. For model checking and simulation purposes the user not only needs to provide the behaviour of the system itself, but also the behaviour of the system environment. For testing, this is not required. Only some additional channels have to be marked as observable, viz. the ones we need to check for in the test derivation algorithm. For details on the Promela specification see [CdR98].

The following two specifications are Promela sources. The first one is the most recent one. The difference is that the first specification has a different implementation of a "nickname change" feature. The IUT does not allow nickname change!

The Most recent version of the Promela conference protocol specification can be obtained here!
The Promela conference protocol specification can be obtained here!

SDL

For the SDL method several specifications of the conference protocol are produced. In the TAU toolset it is possible to use different kinds of test formalisms, e.g. interoperability and conformance testing. For each of these formalisms different specifications are required.

The conference protocol model is specified in a natural way by decomposition the problem into three subprocesses: one for reception and translation of incoming messages, one for managing the conference data structures, and one for composing and broadcasting outgoing PDUs.

Herewith I thank Matthias Runge for translating the SDL specification to Tau 4 format.

An overview of the SDL conference protocol specification in .ps-format can be obtained here!
The SDL conference protocol specification for the TAU 3.4 tool can be obtained here!
The SDL conference protocol specification for the TAU 4 tool can be obtained here!
The General SDL conference protocol specification (.sdl, also known as .pr format) can be obtained here!

From our French colleaques we received the following specifications of the conference protocol. There is a specification of the IUT for local testing and one for remote testing. Both specifications are stored with and without CIF format. The PostScript files for both specifications are also included.

The specification of our French colleagues of the conference protocol in SDL format can be obtained here!

FSM/EFSM

Two EFSM specifications are developed. Both specifications consider a conference protocol entity (IUT) in a context with two other conference protocol entities. The IUT is allowed to participate one of two available conferences. Specification B does also take into account the possibility of a lost data-PDU. Specification C is based on the specifications A and B, and contains some minor changes. Only specification C and D have been used for testing purposes. The difference is that specification D can also setup a conference with only one partner.

The EFSM conference protocol specification (A) can be obtained here!
The EFSM conference protocol specification (B) can be obtained here!
The EFSM conference protocol specification (C) can be obtained here!
The EFSM conference protocol specification (D) can be obtained here!
Prev Table of Contents Next
Chapter 10: Conference Protocol Description Valid HTML 4.01! Chapter 12: Conference Protocol Implementations