Description of a teleconferencing floor control protocol and its implementation

In this paper, we present a formal specification of a teleconferencing floor control protocol and its implementation. The services provided by this protocol are described within the SCCP IETF document (Simple Conference Control Protocol). Finite state machines are used to model services behaviours part of this protocol. Temporal properties are defined as constraints of the teleconferencing system using SCCP protocol. The dynamic properties are described by the LTL logic (Linear Temporal Logic) and verified using the model-checker Spin/Promela. A prototype of a multimedia teleconferencing system is implemented and it is based on the specified protocol. This implementation uses UML notation and is developed with JMF (Java Media Framework) API. (C) 2007 Elsevier Ltd. All rights reserved.