|Formal methods & Tools|
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)!
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!
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!
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!
This page was last updated by Jan Feenstra on 2001-03-22