393
views
0
recommends
+1 Recommend
1 collections
    4
    shares
       
      • Record: found
      • Abstract: found
      • Conference Proceedings: found
      Is Open Access

      An LTL Specification and Verification of a Mobile Teleconferencing System

      proceedings-article

      * , ** , *

      Second International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2008) (VECoS)

      Verification and Evaluation of Computer and Communication Systems

      2 - 3 July 2008

      Mobile Teleconferencing, Control floor, LTL properties, Specification, Verification

      Bookmark

            Abstract

            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.

            Content

            Author and article information

            Contributors
            Conference
            July 2008
            July 2008
            : 1-11
            Affiliations
            [ * ]Laboratoire Alkhawarizmi de Génie Informatique, Université Med-V Souissi

            ENSIAS, Rabat, Morocco
            [ ** ]Ecole supérieure de Technologie Casablanca, Maroc
            Article
            10.14236/ewic/VECOS2008.13
            e8a44381-58cf-4a58-b850-66c3e3e171b8
            © Yassine ELGHAYAM et al. Published by BCS Learning and Development Ltd. Second International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2008)

            This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/

            Second International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2008)
            VECoS
            Leeds, UK
            2 - 3 July 2008
            Electronic Workshops in Computing (eWiC)
            Verification and Evaluation of Computer and Communication Systems
            Product
            Product Information: 1477-9358BCS Learning & Development
            Self URI (journal page): https://ewic.bcs.org/
            Categories
            Electronic Workshops in Computing

            Comments

            Comment on this article