Symbolic Equivalences for Open Systems

Abstract

Behavioural equivalences on open systems are usually defined by comparing system behaviour in all environments. Due to this “universal” quantification over the possible hosting environments, such equivalences are often difficult to check in a direct way. Here, working in the setting of process calculi, we introduce a hierarchy of behavioural equivalences for open systems, building on a previously defined symbolic approach. The hierarchy comprises both branching, bisimulation-based, and non-branching, trace-based, equivalences. Symbolic equivalences are amenable to effective analysis techniques (e.g., the symbolic transition system is finitely branching under mild assumptions), which result to be sound, but often not complete due to redundant information. Two kinds of redundancy, syntactic and semantic, are discussed and and one class of symbolic equivalences is identified that deals satisfactorily with syntactic redundant transitions, which are a primary source of incompleteness.

Paolo Baldan, Andrea Bracciali, Roberto Bruni

Specifying and Verifying UML Activity Diagrams Via Graph Transformation

Abstract

We propose a methodology for system specification and verification based on UML diagrams and interpreted in terms of graphs and graph transformations. Once a system is modeled in this framework, a temporal graph logic can be used to express some of its relevant behavioral properties. Then, under certain constraints, such properties can be checked automatically.The approach is illustrated over a simple case study, the so-called Airport Case Study, which has been widely used along the first two years of the AGILE GC project.

Paolo Baldan, Andrea Corradini, Fabio Gadducci

Mobile UML Statecharts with Localities

Abstract

In this paper an extension of a behavioural subset of UML statecharts for mobile computations is proposed. We study collections of UML objects whose behaviour is given by statecharts. Each object resides in a given place, and a collection of such places forms a network. Objects are aware of the localities of other objects, i.e. the logical names of the places where the latter reside, but not of the physical name of such places. In addition to their usual capabilities, such as sending messages etc., objects can move between places and create and destroy places, which may result in a deep reconfiguration of the network. A formal semantics is presented for this mobility extension which builds upon a core semantics definition of statecharts without mobility which we have used successfully in several contexts in the past years. An example of a model of a network service which exploits mobility for resource usage balance is provided using the proposed extension of UML statecharts.

Diego Latella, Mieke Massink, Hubert Baumeister, Martin Wirsing

Communities: Concept-Based Querying for Mobile Services

Abstract

In this paper, we consider semantic service discovery in a global computing environment. We propose creating a dynamic overlay network by grouping together semantically related services. Each such group is termed a community. Communities are organized in a global taxonomy whose nodes are related contextually. The taxonomy can be seen as an expandable, flexible and distributed semantic index over the system, which aims at improving service discovery. We present a distributed service discovery mechanism that utilizes communities for context-based service discovery. To demonstrate the viability of our approach, we have implemented an infrastructure for supporting communities as well as a prototype application that utilizes communities.

Chara Skouteli, Christoforos Panayiotou, George Samaras, Evaggelia Pitoura

Towards a Formal Treatment of Secrecy Against Computational Adversaries

Abstract

Polynomial time adversaries based on a computational view of cryptography have additional capabilities that the classical Dolev-Yao adversary model does not include. To relate these two different models of cryptography, in this paper we enrich a formal model for cryptographic expressions, originally based on the Dolev-Yao assumptions, with computational aspects based on notions of probability and computational power. The obtained result is that if the cryptosystem is robust enough, then the two adversary models turn out to be equivalent. As an application of our approach, we show how to determine a secrecy property against the computational adversary.

Angelo Troina, Alessandro Aldini, Roberto Gorrieri

For-LySa: UML for Authentication Analysis

Abstract

The DEGAS project aims at enriching standard UML-centred development environments in such a way that the developers of global applications can exploit automated formal analyses with minimal overhead. In this paper, we present For-LySa, an instantiation of the DEGAS approach for authentication analysis, which exploits an existing analysis tool developed for the process calculus LySa. We discuss what information is needed for the analysis, and how to build the UML model of an authentication protocol in such a way that the needed information can be extracted from the model. We then present our prototype implementation and report on some promising results of its use.

Mikael Buchholtz, Carlo Montangero, Lara Perrone, Simone Semprini

Performance Analysis of a UML Micro-business Case Study

Abstract

This paper presents a technique to carry out performance analysis of UML specifications. We consider UML specifications composed of activity, sequence and deployment diagrams. Specifications are translated into the stochastic π-calculus, and quantitative analysis is then performed via the BioSpi tool. The approach is applied to a web-based Micro-business case study.

Katerina Pokozy-Korenblat, Corrado Priami, Paola Quaglia

Efficient Information Propagation Algorithms in Smart Dust and NanoPeer Networks

Abstract

Wireless sensor networks are comprised of a vast number of ultra-small, fully autonomous computing, communication and sensing devices, with very restricted energy and computing capabilities, that co-operate to accomplish a large sensing task. The efficient and robust realization of such large, highly-dynamic and complex networking environments is a challenging algorithmic and technological task.

In this work we present and discuss two protocols for efficient and robust data propagation in wireless sensor networks: LTP (a “local target” optimization protocol) and PFR (a multi-path probabilistic forwarding protocol). Furthermore, we present the NanoPeers architecture paradigm, a peer-to-peer network of lightweight devices, lacking all or most of the capabilities of their computer-world counterparts. We identify the problems arising when applying current routing and searching methods to this nano-world, and present some initial solutions, using a case study of a sensor network instance; Smart Dust.

Sotiris Nikoletseas, Paul Spirakis

The Kell Calculus: A Family of Higher-Order Distributed Process Calculi

Abstract

This paper presents the Kell calculus, a family of distributed process calculi, parameterized by languages for input patterns, that is intended as a basis for studying component-based distributed programming. The Kell calculus is built around a π-calculus core, and follows five design principles which are essential for a foundational model of distributed and mobile programming: hierarchical localities, local actions, higher-order communication, programmable membranes, and dynamic binding. The paper discusses these principles, and defines the syntax and operational semantics common to all calculi in the Kell calculus family. The paper provides a co-inductive characterization of contextual equivalence for Kell calculi, under sufficient conditions on pattern languages, by means of a form of higher-order bisimulation called strong context bisimulation. The paper also contains several examples that illustrate the expressive power of Kell calculi.

Alan Schmitt, Jean-Bernard Stefani

A Software Framework for Rapid Prototyping of Run-Time Systems for Mobile Calculi

Abstract

We describe the architecture and the implementation of the Mikado software framework, that we call IMC (Implementing Mobile Calculi). The framework aims at providing the programmer with primitives to design and implement run-time systems for distributed process calculi. The paper describes the four main components of abstract machines for mobile calculi (node topology, naming and binding, communication protocols and mobility) that have been implemented as Java packages. The paper also contains the description of a prototype implementation of a run-time system for the Distributed Pi-Calculus relying on the presented framework.

Lorenzo Bettini, Rocco De Nicola, Daniele Falassi, Marc Lacoste, Luís Lopes, Licínio Oliveira, Hervé Paulino, Vasco T. Vasconcelos

A Generic Membrane Model (Note)

Abstract

In this note we introduce a generic model for controlling migration in a network of distributed processes. To this end, we equip the membrane of a domain containing processes with some computing power, including in particular some specific primitives to manage the movements of entities from the inside to the outside of a domain, and conversely. We define a π-calculus instance of our model, and illustrate by means of examples its expressive power. We also discuss a possible extension of our migration model to the case of hierarchically organized domains.

Gérard Boudol

A Framework for Structured Peer-to-Peer Overlay Networks

Abstract

Structured peer-to-peer overlay networks have recently emerged as good candidate infrastructure for building novel large-scale and robust Internet applications in which participating peers share computing resources as equals. In the past three year, various structured peer-to-peer overlay networks have been proposed, and probably more are to come. We present a framework for understanding, analyzing and designing structured peer-to-peer overlay networks. The main objective of the paper is to provide practical guidelines for the design of structured overlay networks by identifying a fundamental element in the construction of overlay networks: the embedding of k–ary trees. Then, a number of effective techniques for maintaining these overlay networks are discussed. The proposed framework has been effective in the development of the DKS system, whose preliminary design appears in [2].

Luc Onana Alima, Ali Ghodsi, Seif Haridi

Verifying a Structured Peer-to-Peer Overlay Network: The Static Case

Abstract

Structured peer-to-peer overlay networks are a class of algorithms that provide e.cient message routing for distributed applications using a sparsely connected communication network. In this paper, we formally verify a typical application running on a .xed set of nodes. This work is the foundation for studies of a more dynamic system.

We identify a value and expression language for a value-passing CCS that allows us to formally model a distributed hash table implemented over a static DKS overlay network. We then provide a speci.cation of the lookup operation in the same language, allowing us to formally verify the correctness of the system in terms of observational equivalence between implementation and speci.cation. For the proof, we employ an abstract notation for reachable states that allows us to work conveniently up to structural congruence, thus drastically reducing the number and shape of states to consider. The structure and techniques of the correctness proof are reusable for other overlay networks.

Johannes Borgström, Uwe Nestmann, Luc Onana, Dilian Gurov

A Physics-Style Approach to Scalability of Distributed systems

Abstract

Is it possible to treat large scale distributed systems as physical systems? The importance of that question stems from the fact that the behavior of many P2P systems is very complex to analyze analytically, and simulation of scales of interest can be prohibitive. In Physics, however, one is accustomed to reasoning about large systems. The limit of very large systems may actually simplify the analysis. As a first example, we here analyze the effect of the density of populated nodes in an identifier space in a P2P system. We show that while the average path length is approximately given by a function of the number of populated nodes, there is a systematic effect which depends on the density. In other words, the dependence is both on the number of address nodes and the number of populated nodes, but only through their ratio. Interestingly, this effect is negative for finite densities, showing that an amount of randomness somewhat shortens average path length.

Erik Aurell, Sameh El-Ansary

BGP-Based Clustering for Scalable and Reliable Gossip Broadcast

Abstract

This paper presents a locality-based dissemination graph algorithm for scalable reliable broadcast. Our algorithm scales in terms of both network and memory usage. Processes only have “local knowledge” about each other. They organize themselves dynamically (right from the bootstrapping phase), according to join, leave or crash events, to form a locality-based dissemination graph. Broadcast messages can be disseminated using these graphs in large networks like the Internet, without relying on any special infrastructure or intermediate brokers. Roughly speaking, a dissemination graph consists of “non-crossing” (independent) trees that provide multiple paths between processes for improved broadcast efficiency and reliability. Each tree is constructed using BGP routing information about process “locality”. We convey the feasibility of the algorithm using both simulation and experimental results and describe an application of our algorithm for broadcasting information streams.

M. Brahami, P. Th. Eugster, R. Guerraoui, S. B. Handurukande

Trust Lifecycle Management in a Global Computing Environment

Abstract

In a global computing environment in order for entities to collaborate, they should be able to make autonomous access control decisions with partial information about their potential collaborators. The SECURE project addresses this requirement by using trust as the mechanism for managing risks and uncertainty. This paper describes how trust lifecycle management, a procedure of collecting and processing evidence, is used by the SECURE collaboration model. Particular emphasis is placed on the processing of the evidence and the notion of attraction. Attraction considers the effects of evidence about the behaviour of a particular principal on its current trust value both in terms of trustworthiness and certainty and is one of the distinctive characteristics of the SECURE collaboration making it more appropriate for a global computing setting.

S. Terzis, W. Wagealla, C. English, P. Nixon

The SOCS Computational Logic Approach to the Specification and Verification of Agent Societies

Abstract

This article summarises part of the work done during the first two years of the SOCS project, with respect to the task of modelling interaction amongst CL-based agents. It describes the SOCS social model: an agent interaction specification and verification framework equipped with a declarative and operational semantics, expressed in terms of abduction. The operational counterpart of the proposed framework has been implemented and integrated in SOCS-SI, a tool that can be used for on-the-fly verification of agent compliance with respect to specified protocols.

Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello, Paolo Torroni

The KGP Model of Agency for Global Computing: Computational Model and Prototype Implementation

Abstract

We present the computational counterpart of the KGP (Knowledge, Goals, Plan) declarative model of agency for Global Computing. In this context, a computational entity is seen as an agent developed using Computational Logic tools and techniques. We model a KGP agent by relying upon a collection of capabilities, which are then used to define a collection of transitions, to be used within logically specified, context sensitive control theories, which we call cycle theories. In close relationship to the declarative model, the computational model mirrors the logical architecture by specifying appropriate computational counterparts for the capabilities and using these to give the computational models of the transitions. These computational models and the one specified for the cycle theories are all based on, and are significant extensions of, existing proof procedures for abductive logic programming and logic programming with priorities. We also discuss a prototype implementation of the overall computational model for KGP.

A. Bracciali, N. Demetriou, U. Endriss, A. Kakas, W. Lu, P. Mancarella, F. Sadri, K. Stathis, G. Terreni, F. Toni

Springer Professional

Global Computing

IST/FET International Workshop, GC 2004 Rovereto, Italy, March 9-12, 2004 Revised Selected Papers

Inhaltsverzeichnis

Frontmatter

Symbolic Equivalences for Open Systems

Specifying and Verifying UML Activity Diagrams Via Graph Transformation

Mobile UML Statecharts with Localities

Communities: Concept-Based Querying for Mobile Services

Towards a Formal Treatment of Secrecy Against Computational Adversaries

For-LySa: UML for Authentication Analysis

Performance Analysis of a UML Micro-business Case Study

Efficient Information Propagation Algorithms in Smart Dust and NanoPeer Networks

The Kell Calculus: A Family of Higher-Order Distributed Process Calculi

A Software Framework for Rapid Prototyping of Run-Time Systems for Mobile Calculi

A Generic Membrane Model (Note)

A Framework for Structured Peer-to-Peer Overlay Networks

Verifying a Structured Peer-to-Peer Overlay Network: The Static Case

A Physics-Style Approach to Scalability of Distributed systems

BGP-Based Clustering for Scalable and Reliable Gossip Broadcast

Trust Lifecycle Management in a Global Computing Environment

The SOCS Computational Logic Approach to the Specification and Verification of Agent Societies

The KGP Model of Agency for Global Computing: Computational Model and Prototype Implementation

Backmatter

Premium Partner