In the computer-supported cooperative work domain, researchers have always wondered about which principles and models to adopt for the development of collaborative applications capable to really meet users' needs. However, these requirements are often unpredictable and depend on several task- or environment-related factors. Integrated collaborative environments are rarely open, extensible, and reconfigurable enough so as to meet these requirements. This paper presents an environment, called loosely coupled environment for integrating collaborative applications (LEICA), allowing the integration of existing collaborative applications. LEICA adopts a loosely coupled integration approach which is based on Web Services technology, an Event Notification System, and the definition of Collaboration Policies to control the interactions between integrated applications. LEICA allows different functionalities of existing applications to be dynamically combined and controlled, enhancing its flexibility. Through a case study, we show how LEICA was successfully used to integrate three collaborative applications: a Co-browsing tool, an instant messaging tool, and a Voice over Internet Protocol Conference Controller.

Widespread adoption of Web technologies, particularly in professional and educational areas, has motivated new research efforts with the objective of designing new interaction mechanisms based on Web technologies. Within this framework, collaborative Web browsing (cobrowsing) aims at extending currently available Web browsing capabilities in order to allow several users to "browse together" on the Web. Such a browsing paradigm can have many useful applications, for instance, in e-learning, for collaboratively searching and retrieving documents, and for online assistance (helpdesk). A cobrowsing system should provide all the facilities required for allowing users to establish and release, in a very simple and flexible way, browsing synchronization relations as well as interactions with continuous media presentations embedded within Web pages. This paper presents the design, modeling, and implementation of the cobrowsing system called CoLab. CoLab provides all the functionalities required for allowing users to collaboratively browse the Web, and a first experimental version of the tool has been implemented and is fully operational

Collaborative Web browsing aims at extending currently available Web browsing capabilities in order to allow several users getting their browsing activity synchronized. This is a new and promising research area whose possibilities have not yet been exhaustively covered. From our point of view a collaborative Web browsing system should provide all the necessary facilities to allow users to get synchronized and desynchronized in a flexible way. Synchronization relies on a simple authorization protocol through which users can invite other users to create and release browsing synchronization relations. Additionally, special synchronization operatorsy intends to use by privileged users, are also proposed with the purpose of overriding the authorization protocol. In this paper we present our proposal for modeling and implementing a Collaborative Web Browsing system called CoLab, which has been developed using Java/spl trade/ technology; we present the main features of our current development prototype: CoLab 2.0.

The formal description technique RT-LOTOS has been selected as intermediate language to add formality to a real-time UML profile named TURTLE. For this sake, an RT-LOTOS verification platform has been developed for early detection of design errors in real-time system models. The paper discusses an extension of the platform by inclusion of verification tools developed for time Petri nets. The starting point is the definition of RT-LOTOS to TPN translation patterns. In particular, we introduce the concept of components embedding time Petri nets. The translation patterns are implemented in a prototype tool which takes as input an RT-LOTOS specification and outputs a TPN in the format admitted by the TINA tool. The efficiency of the proposed solution has been demonstrated on various case studies.

We present a UML 1.5 profile named TURTLE (Timed UML and RT-LOTOS Environment) endowed with a formal semantics given in terms of RT-LOTOS. TURTLE relies on UML's extensibility mechanisms to enhance class and activity diagrams. Class diagrams are extended with specialized classes named Tclasses, which communicate and synchronize through gates. Also, associations between Tclasses are attributed by a composition operator (Parallel, Synchro, Invocation, Sequence, or Preemption) which provides them with a formal semantics. TURTLE extends UML activity diagrams with synchronization actions and temporal operators (deterministic delay, nondeterministic delay, time-limited offer, and time-capture). The real-time dimension of TURTLE has been further improved by the addition of two composition operators, periodic and suspend, as well as suspendable delay, latency, and time-limited offer operators at the activity diagram level. Core characteristics of TURLE are supported by TTool - the TURTLE toolkit - which includes a diagram editor, a RT-LOTOS code generator and a result analyzer. The toolkit reuses RTL, a RT-LOTOS validation tool offering debug-oriented simulation and exhaustive analysis. TTool hides RT-LOTOS to the end-user and allows him/her to directly check TURTLE modeling against logical errors and timing inconsistencies. Besides the foundations of the TURTLE profile, this paper also discusses its application in the context of space-based embedded software.

The concept of collaborative browsing (CB) introduced here including a short presentation of CoLab, a Java environment implementing a CB solution. The applicability of CoLab is discussed for e-learning and a possible application scenario is sketched.

With the growing demand for collaboration technologies, several CSCW (computer-supported cooperative work) systems have been developed. CVEs (collaborative virtual environments) represent an important category of CSCW systems that generally make use of 3D shared space to provide collaboration facilities. However in most CVEs collaboration is restricted to the virtual reality context. In this paper, it is proposed to extend CVEs through the integration of different collaboration tools in order to allow collaboration to take place in different contexts (e.g. Web browsing), in a parallel and coordinated way with the virtual scene.

This paper presents a methodology to provide the formal verification, scheduling and presentation of consistent SMIL 2.0 documents. The second version of SMIL provides a temporal model much more flexible enabling the author to specify synchronization constraints that can not be potentially satisfied during the presentation of his document. For this reason, some types of inconsistency that can be produced in a SMIL 2.0 document are characterized in this paper and the effect of these inconsistencies were analysed using some SMIL 2.0 players. Furthermore, some results are also presented in order to provide a consistent diagnosis of the verification analysis based on a simple and operational scheduling graph.

The utilization of Interactive Multimedia Documents (IMDs) has been largely addressed in several fields such as education, medicine, etc. since these documents can be distributed and accessed over the World-Wide-Web. In this context, the W3C standard Synchronized Multimedia Integration Language (SMIL) has been proposed for the presentation of IMD's over the Web. However, the flexibility of the temporal model of SMIL 2.0 allows the author to describe temporal synchronization relationships that potentially can not be resolved during the presentation of the document, known as temporal inconsistencies. For this reason, an approach that enables to detect and correct these inconsistencies is needed.This paper presents a formal approach for the verification, scheduling and presentation of consistent SMIL 2.0 documents based on the RT-LOTOS formal description technique. Thus, the consistency analysis of SMIL 2.0 documents is presented and some solutions are proposed in order to deal with potential state space explosion problems. Further on, some contributions are also presented concerning the scheduling and presentation of SMIL 2.0 documents based on a simple scheduling graph, called a Time Labeled Automata (TLA), derived automatically from the document formal specification. Finally, a global Java-based architecture for the implementation of a player of consistent SMIL 2.0 documents is presented.

The past years have seen the emergence of cooperative applications that require the exchange of high volumes of data among remote cooperating parties. With the purpose of providing a scalable communication solution for this kind of applications, multicast transport protocols have been proposed in the literature, because point to point communications lead to wasting too much bandwidth, in particular if one wants to guarantee a certain level of reliability. In this paper, we study a multicast transport protocol, scalable probabilistic reliable multicast (SPRM), and show how a formal description technique, RT-LOTOS, has been successfully applied to identify some flaws in this complex multi-parties protocol. It is shown how the same approach may also be used for performance evaluation, and we compare our results with other models based on queuing theory.

The paper generalizes previous works of the authors by revisiting the concept of temporal consistency of hypermedia documents. This generalization relies on the distinction of internal and external non-deterministic events.

Hypermedia authoring tools usually suffer ikom a lack of validation capabilities that would make it possible to check a document against temporal inconsistencies.The document design methodology proposed in the paper overcomes this problem by translating a high-level model of an hypermedia document into a RT-LOTOS formal specificatio~on which standard reachability analysis may be applied for verification purposes.The propod approa~extends an early work to verify both intrinsic and extrinsic temporal consistency properties of an hypermedia documenti 1.1

The paper presents a methodology by which documents authored with the Nested Context Model (NCM) are automatically translated into a RT-LOTOS specification. The latter is then checked against intrinsic and extrinsic consistencies using standard RT-LOTOS reachability analysis.

This paper introduces a new synchronization model for the formal specification of multimedia documents. By this approach, an user is able to formalize his document by hierarchically composing a set of presentation and constraint objects which are then automatically translated into a complete RT-LOTOS formal specification (RT-LOTOS is a temporal extension of the standard LOTOS Formal Description Technique) . Verification of a multimedia document aiming to identify potential temporal inconsistencies is then performed using standard reachability analysis developed and implemented for RT-LOTOS. KEYWORDS Multimedia-Hypermedia, Temporal Synchronization, Formal Specification and Verification, LOTOS, RT-LOTOS INTRODUCTION Multimedia documents represent a powerful method of communication integrating a variety of media with different temporal characteristics, e.g. time dependent media such as video, audio or animation, and time independent media, such as text, graphics and images. A central i...

Designing distributed multimedia applications raises temporal and spatial synchronization issues related to processing, transport, storage, retrieval and presentation of data, sound, still images and video. Within this framework, the paper aims to define a general-purpose multimedia synchronization mechanism, known as the conditional delivery mechanism, capable of addressing both intraand inter-stream synchronization issues. The proposed mechanism, based on the identification of causal relations among information units of one or several streams, is designed to ensure that these causal relations, expressed at the user's level, are satisfied when delivering the streams. The conditional delivery mechanism is analyzed in depth and both informal and formal specifications of the mechanism are provided. The formal specification refers to an extension of the standard formal description technique LOTOS (RT-LOTOS for real-time LOTOS). Validation results of the conditional delivery mechanism are finally presented for a distance and interactive training application.

The design of a distributed multimedia application involves both temporal and spatial synchronization problems related to the processing, transport, storage, retrieval and presentation of data, sound, still images and video. Within this general framework, the paper aims at defining a new multimedia synchronization mechanism, the so-called conditional delivery mechanism, which appears particularly useful for achieving both intra- and inter-stream synchronization. Main motivations behind this synchronization mechanism are first discussed on a simple example, namely a distributed application in the area of distance and interactive training, and then the details of the mechanism are presented. This presentation starts with an informal discussion on simple examples, which is followed by a formal specification of the mechanism based on the use of a temporal extension of the Formal Description Technique LOTOS.

Proposes the observer concept for designing self-checking distributed systems, i.e. systems that detect erroneous behaviors as soon as errors act at some observable output level. The approach provides a solution to build systems whose on-line behavior is checked against a formal model derived from a formal description. In other words, the actual implementation is continuously checked against a reference, this reference being a formal and verified model of some adequately selected aspects of the system behavior. The corresponding methodology, the software concepts and some applications of the observer are presented. General definitions are given first that theoretically define self-checking systems as systems that include and implement complete on-line validation. The basic concepts and the difficulties to implement self-checking validation are then given. In order to provide simple implementations, the previous definitions are weakened to design quasi-self-checking observers for LANs using a broadcast service. Three specific applications are given to illustrate the proposed approach: testing a virtual ring MAC protocol, checking the link and transport layers in an industrial LAN, and managing a complete OSI layering, from layer 2 to layer 6, in an open system architecture.>

This paper presents a fault-tolerant distributed system designed for real-time control applications (REBUS), which is one of the research basis of the industrial real-time system MODUMAT 800. It is made up of functional units, i.e., programmable multiloop regulators and operator displays, linked together by a communication structure. The communication hardware consists of a set of serial bus interface boards, one per functional unit, loosely coupled together by a double serial bus and linked to their functional units by a private parallel bus.