An LTL Specification and Verification of a Mobile

Portable computing devices with wireless communication interfaces such as PDAs or smart phones led to the emerging of applications and services that support communication and collaboration among mobile users. In this paper we focus on the collaborative applications that allow a group of users, geographically distributed, to work together. In particular a teleconferencing system is an example of a collaborative application where remote users may interact to accomplish a common goal. Therefore, the teleconference owner may initiate a session, which is then joined and left dynamically by the involved group members. The teleconferencing collaborative system over a mobile network provides tools for communication between group members while allowing them to share information and collaborate with each other. Collaboration in a mobile condition poses new challenges, such as host mobility, limited device resources, and intermittent connectivity. The group members are frequently opposed to disconnections during the collaboration session. A user might become temporarily unavailable even though he or she is still engaged in the collaboration session. The contribution of this paper is two fold. First we describe a formal specification of a teleconferencing system over a mobile network. This specification allowed us to define a set of important properties of the teleconferencing system dynamic behaviour. Second we formalize these properties using LTL logic while distinguishing between the required properties for the floor control and those related to the mobility requirements