Catálogo de publicaciones - libros

A fundamental problem in the area of service engineering is the so-called cross-cutting nature of services, i.e., that service behavior results from a collaboration of partial component behaviors. We present an approach for model-based service engineering, in which system component models are derived automatically from collaboration models. These are specifications of sub-services incorporating both the local behavior of the components and the necessary inter-component communication. The collaborations are expressed in a compact and self-contained way by UML collaborations and activities. The UML activities can express service compositions precisely, so that components may be derived automatically by means of a model transformation. In this paper, we focus on the important issue of how to coordinate and compose collaborations that are executed with several sessions at the same time. We introduce an extension to activities for session selection. Moreover, we explain how this composition is mapped onto the components and how it can be translated into executable code.

This paper deals with the analysis and design of a computer network simulator for educational purposes. The SOMT method based on object-oriented analysis and SDL design has been used for that purpose. The simulator developed allows protocol descriptions independent of event management mechanisms and run-time network topology configuration without modifying the SDL description of the system developed.

UML supports a multi-view modeling approach for overcoming software complexity. It consists of several diagrams, which allow for considering software systems from different perspectives: structure, behavior and deployment. However, this multi-view approach faces the challenging issue of consistency. Moreover, when UML is used for real-time systems, through its specialized profiles such as UML/SPT for instance, the consistency issue becomes more complex. New aspects, relevant for real-time systems design, should be taken into consideration. These include concurrency, time constraints and schedulability. In this paper, we present a consistency framework for UML/SPT models. This framework addresses incrementally the various aspects of consistency including syntactic, semantic, concurrency-related and time consistency. In this framework, we introduce an approach for checking time consistency between statecharts and sequence diagrams using schedulability analysis.

Scenario-driven requirement specifications are widely used to capture and represent functional requirement. More recently, the Use Case Maps language (UCM), being standardized by ITU-T as part of the User Requirements Notation (URN) has gained on popularity within the software requirements community. UCM models focus on the description of functional and behavioral requirements as well as high-level designs at the early stages of system development processes. However, timing issues are often overlooked during the initial system design and treated as non-related behavioral issues and described therefore in separate models. We believe that timing aspects must be integrated into the system model during early development stages. In this paper, we present a novel approach to describe timing constraints in UCM specifications. We describe a formal operational semantics of Timed UCM in terms of Timed Automata (TA) that can be analyzed and verified with the UPPAAL model checker tool. Our approach is illustrated using a case study of the IP Multicast Routing Protocol.

Telecommunication services will be in the future built upon peer-to-peer protocols. This implies the need to have strong guarantees of the dependability of those protocols. One building block for such protocols are distributed hash tables (DHT in short), and Pastry is a protocol implementing distributed hash tables. We have designed a probabilist model of Pastry that enabled us to simulate it. In particular, we have studied the performance of the protocol with respect to the number of nodes. We have used for this study probabilistic model checking tools used in the RNTL project Averros. This is a significant application of academic tools to industrial concerns.

OpenComRTOS is one of the few Real-Time Operating Systems (RTOS) for embedded systems that was developed using formal modeling techniques. The goal was to obtain a proven trustworthy component with a clean and high performance architecture useable on a wide range of networked embedded systems. The result is a scalable communication system with real-time capabilities. Besides a rigorous formal verification of the kernel algorithms, the resulting architecture has several properties that enhance the safety and real-time properties of the RTOS. The code size in particular is very small and typically 10 times less than a typical equivalent single processor RTOS.

Using a common model for both functional verification and performance evaluation of a network protocol will reduce a considerable amount of protocol development time and cost. Although there have been several researches trying to achieve this goal, they have not been used widely yet especially in industry. This paper shows a case study in SDL design and performance evaluation of a wireless and mobile technology. In order to evaluate our mobility management technique for 3GPP LTE systems, we designed a simple 3GPP LTE system and its mobility performance system with pure SDL and Tau performance library. This paper describes our experience in pure SDL-based performance evaluation with Tau and discusses SDL design and simulation issues for more efficient performance evaluation with SDL.