Catálogo de publicaciones - libros
Formal Methods for Mobile Computing: 5th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-Moby 2005, Bertinoro, Italy, April 26-30, 2005, Advanced Lectures
Marco Bernardo ; Alessandro Bogliolo (eds.)
Resumen/Descripción – provisto por la editorial
No disponible.
Palabras clave – provistas por la editorial
No disponibles.
Disponibilidad
Institución detectada | Año de publicación | Navegá | Descargá | Solicitá |
---|---|---|---|---|
No detectada | 2005 | SpringerLink |
Información
Tipo de recurso:
libros
ISBN impreso
978-3-540-25697-7
ISBN electrónico
978-3-540-32021-0
Editor responsable
Springer Nature
País de edición
Reino Unido
Fecha de publicación
2005
Información sobre derechos de publicación
© Springer-Verlag Berlin Heidelberg 2005
Cobertura temática
Tabla de contenidos
doi: 10.1007/11419822_1
History-Dependent Automata: An Introduction
Ugo Montanari; Marco Pistore
In this paper we give an overview of History Dependent Automata, an extension of ordinary automata that overcomes their limitations in dealing with named calculi. In a named calculus, the observations labelling the transitions of a system may contain names which represent features such as communication channels, node identifiers, or the locations of the system. An example of named calculus is -calculus, which has the ability of sending channel names as messages and thus of dynamically reconfiguring process acquaintances and of modeling agents and code mobility. We show that History-Dependent Automata allow for a compact representation of -calculus processes which is suitable both for theoretical investigations and for practical purposes such as verification.
I - Models and Languages | Pp. 1-28
doi: 10.1007/11419822_2
Mobile Distributed Programming in
Lorenzo Bettini; Rocco De Nicola
Network-aware computing has called for new programming languages that exploit the mobility paradigm as a basic interaction mechanism. In this paper we present , an experimental programming language specifically designed to program distributed systems composed of several components interacting through multiple distributed tuple spaces and mobile code. The language consists of a set of coordination primitives inspired by Linda, a set of operators for building processes borrowed from process algebras and a few classical constructs for sequential programming. naturally supports programming with explicit localities; these are first-class data that can be manipulated like any other data, and coordination primitives that permit controlling interactions among located processes. Via a series of examples, we show that many mobile code programming paradigms can be naturally implemented by means of the considered language.
I - Models and Languages | Pp. 29-68
doi: 10.1007/11419822_3
Dealing with Node Mobility in Ad Hoc Wireless Network
Mario Gerla; Ling-Jyh Chen; Yeng-Zhong Lee; Biao Zhou; Jiwei Chen; Guang Yang; Shirshanka Das
A Mobile “Ad hoc” wireless NETwork (MANET) is a network established for a special, often extemporaneous service customized to applications. The ad hoc network is typically set up for a limited period of time, in an environment that may change from application to application. As a difference from the Internet where the TCP/IP protocol suite supports a vast range of applications, in the MANET the protocols are tuned to a specific customer and application (eg, send a video stream across the battlefield; find out if there is a fire in the forest; establish a videoconference among several teams engaged in a rescue effort, etc). The customers move and the environment may change dynamically and unpredictably. For the MANET to retain its efficiency, the ad hoc protocols at various layers may need to self-tune to adjust to environment, traffic and mission changes. From these properties emerges the vision of the MANET as an extremely flexible, malleable and yet robust and formidable network architecture. Indeed, an architecture that can be deployed to monitor the habits of birds in their natural habitat, and which, in other circumstances, can be organized to interconnect rescue crews after a Tsunami disaster, or yet can be structured to launch deadly attacks onto unsuspecting enemies.
II - Scalability and Performance | Pp. 69-106
doi: 10.1007/11419822_4
Performance Analysis of Mobile Systems
Vincenzo Grassi
Mobile systems, where both computing nodes and software components can dynamically change their location, are already a reality, thanks to technological advances in several related fields. The high variability and heterogeneity of these systems raises severe performance problems, thus requiring a careful planning of any performance validation activity concerning these systems. This paper reviews some approaches that have been proposed to this end, presenting them within a general framework aimed at supporting a systematic approach to the validation of non functional attributes. In this framework we emphasize that one of the key points for the actual and effective introduction of non-functional attributes validation since the early design phases is the definition of from design-oriented models to analysis-oriented models.
II - Scalability and Performance | Pp. 107-154
doi: 10.1007/11419822_5
A Methodology Based on Formal Methods for Predicting the Impact of Dynamic Power Management
A. Acquaviva; A. Aldini; M. Bernardo; A. Bogliolo; E. Bontà; E. Lattanzi
One of the major issues in the design of a mobile computing device is reducing its power consumption. A commonly used technique is the adoption of a dynamic power management policy, which modifies the power consumption of the device based on certain run time conditions. The introduction of the dynamic power management within a battery-powered device may not be transparent, as it may alter the overall system behavior and efficiency. Here we present a methodology that can be used in the early stages of the system design to predict the impact of the dynamic power management on the system functionality and performance. The predictive methodology, which relies on formal methods to compare the properties of the system without and with dynamic power management, is illustrated through the application of its various phases to a simple example of power-manageable system.
III - Dynamic Power Management | Pp. 155-189
doi: 10.1007/11419822_6
Dynamic Power Management Strategies Within the IEEE 802.11 Standard
Andrea Acquaviva; Edoardo Bontà; Emanuele Lattanzi
Mobile terminals such as cellular phones, smart phones and PDAs require wireless connection to exchange information with the external world. In this tutorial we focus on wireless packet networks based on the IEEE 802.11b protocol, commonly used to build local area networks of palmtop and notebook computers. Due to limited battery lifetime of mobile terminals, energy consumption of wireless interfaces becomes a critical design constraint. Within the IEEE 802.11 standard, power conservation protocols have been implemented that trade power for performance. In this tutorial, we present a power-accurate model of wireless network interface card that allows the power/performance trade-off to be studied as a function of traffic patterns imposed by the applications. The model has been validated against measurements on real hardware devices.
III - Dynamic Power Management | Pp. 190-214
doi: 10.1007/11419822_7
Network Swapping
Emanuele Lattanzi; Andrea Acquaviva; Alessandro Bogliolo
Wireless mobile terminals have limited storage memory due to weight, size and power constraints. Potentially unlimited virtual memory could be found on remote servers made accessible through a wireless link, but power hungry wireless network interface cards (WNIC) may reduce the battery lifetime if not efficiently exploited, actually limiting the practical interest of network virtual memory (NVM). On the other hand, when network memory is used for swapping, service performance can be an issue. In this tutorial we discuss the feasibility of network swapping for wireless mobile terminals. First, we perform extensive experiments to compare performance and energy of network swapping with those of local swapping on microdrives and flash memories. Our results show that remote swap devices made accessible through a power-manageable WNIC can be even more efficient than local microdrives. Second, we address the issue of mobility management by presenting an infrastructure providing efficient remote memory access to mobile terminals. We report experimental results obtained on a working prototype of the proposed infrastructure.
IV - Middleware Support | Pp. 215-233
doi: 10.1007/11419822_8
Hermes: Agent-Based Middleware for Mobile Computing
Flavio Corradini; Emanuela Merelli
Hermes is a middleware system for design and execution of activity-based applications in distributed environments. It supports mobile computation as an application implementation strategy. While middleware for mobile computing has typically been developed to support physical and logical mobility, Hermes provides an integrated environment where application domain experts can focus on designing activity workflow and ignore the topological structure of the distributed environment. Generating mobile agents from a workflow specification is the responsibility of a context-aware compiler.
Hermes is structured as a component-based, agent-oriented system with a 3-layer software architecture. It can be configured for specific application domains by adding domain-specific component libraries. The Hermes middleware layer, compilers, libraries, services and other developed tools together result in a very general programming environment, which has been validated in two quite disparate application domains, one in industrial control and the other in bioinformatics. In the industrial control domain, embedded systems with scarce computational resources control product lines. Mobile agents are used to trace products and support self-healing. In the bionformatics domain, mobile agents are used to support data collection and service discovery, and to simulate biological system through autonomous components interactions.
IV - Middleware Support | Pp. 234-270