Formal Methods and Tools Formal methods & Tools University of Twente

 
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.

LOTOS conference protocol IUT specificationThe LOTOS conference protocol IUT specification can be obtained here!
LOTOS conference protocol SUT specification for LITEThe LOTOS conference protocol SUT specification can be obtained here (LITE, library mod-is)!
LOTOS conference protocol SUT specification for CADP97bThe LOTOS conference protocol SUT specification can be obtained here (CADP97b)!
LOTOS conference protocol SUT specification for CADP99dThe 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!

Promela conference protocol IUT specificationThe Most recent version of the Promela conference protocol specification can be obtained here!
Promela conference protocol IUT specificationThe 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.

SDL conference protocol IUT specification overview in .ps formatAn overview of the SDL conference protocol specification in .ps-format can be obtained here!
SDL TAU 3.4 conference protocol IUT specification source filesThe SDL conference protocol specification for the TAU 3.4 tool can be obtained here!
SDL TAU 4 conference protocol IUT specification source filesThe SDL conference protocol specification for the TAU 4 tool can be obtained here!
General SDL conference protocol IUT specification source filesThe 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.
SDL conference protocol IUT specificationThe 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.

EFSM conference protocol IUT specificationThe EFSM conference protocol specification (A) can be obtained here!
EFSM conference protocol IUT specificationThe EFSM conference protocol specification (B) can be obtained here!
EFSM conference protocol IUT specificationThe EFSM conference protocol specification (C) can be obtained here!
EFSM conference protocol IUT specificationThe EFSM conference protocol specification (D) can be obtained here!

This page was last updated by Jan Feenstra on 2001-03-22