Catálogo de publicaciones - libros

We study the problems related to querying large, distributed XML documents. Our proposal takes the form of a new process calculus in which XML data are processes that can be queried by means of concurrent pattern-matching expressions. What we achieve is a functional, strongly-typed programming model based on three main ingredients: an asynchronous process calculus that draws features from -calculus and concurrent-ML; a model where both documents and expressions are represented as processes, and where evaluation is represented as a parallel composition of the two; a static type system based on regular expression types.

Model transformations, like refinement or refactoring, have to respect the semantics of the models transformed. In the case of behavioural models this semantics can be specified by transformations, too, describing an abstract interpreter for the language. Both kinds of transformations, if given in a rule-based way, can formally be described as graph transformations.

In this paper, we present executable business processes, their operational semantics and refactoring, as an example of this fact. Using results from graph transformation theory about critical pairs and local confluence, we show that our transformations preserve the semantics of processes. The analysis is performed by means of the graph transformation tool AGG.

A central point when integrating services concerns to the description, agreement and enforcement of the quality aspect of service interaction, usually known as Service Level Agreement (SLA). This paper presents a framework for SLA negotiation based on fuzzy sets. We propose (i) a request language for clients to describe quality preferences, (ii) a publication language for providers to define the qualities of their offered services, and (iii) a decision procedure for granting any client request with a SLA contract fitting the requestor requirements. We start with a restricted framework in which the different qualities of a service are handled independently (as being orthogonal) and then we propose an extension that allows clients and providers to express dependencies among different qualities.

We study a problem of scheduling client requests to servers. Each client has a particular latency requirement at each server and may choose either to be assigned to some server in order to get serviced provided that her latency requirement is met or not to participate in the assignment at all. From a global perspective, in order to optimize the performance of such a system, one would aim to maximize the number of clients that participate in the assignment. However, clients may behave selfishly in the sense that each of them simply aims to participate in an assignment and get serviced by some server where her latency requirement is met with no regard to the overall system performance. We model this selfish behavior as a strategic game, show how to compute equilibria efficiently, and assess the impact of selfishness on system performance. We also show that the problem of optimizing performance is computationally hard to solve, even in a coordinated way, and present efficient approximation and online algorithms.

Intuitively, a cache-oblivious algorithm implements an adaptive strategy which runs efficiently on any memory hierarchy without requiring previous knowledge of the parameters of the hierarchy. For this reason, cache-obliviousness is an attractive feature of an algorithm meant for a global computing environment, where software may be run on a variety of different platforms for load management purposes. In this paper we present a negative result on cache-obliviousness, namely, we show that an optimal cache-oblivious algorithm for the fundamental primitive of matrix transposition cannot exist without the assumption, which forces the (unknown) parameters of the memory hierarchy to satisfy a certain technical relation. Our contribution specializes the result of Brodal and Fagerberg for general permutations to matrix transposition, and provides further evidence that the tall cache assumption is often necessary to attain optimality in the context of cache-oblivious algorithms.

Remote internet voting incorporates many of the core challenges of trusted global computing. In this paper, we present the Kiezen op Afstand (KOA) system. KOA is a Free Software, remote voting system developed for the Dutch government in 2003/2004. In addition to being Open Source, it is also partially formally specified and verified. This paper summarises the work carried out to date on the KOA system. It charts the evolution of the system, from its initial conception by the Dutch Government, through to its current status. It also describes a roadmap of milestones towards completing its next release: a Free Software, general-purpose, formally specified and verified internet voting system, that incorporates Proof Carrying Code technology for software update and allows trustworthy voting from a mobile phone. We propose that the KOA system should be used as an for research in electronic and internet voting; we are saying that we have solved any of the major problems inherent in voting with computers.

We describe a type system for the X calculus, introduced in [8]. An X-network is a network of locations, where each location consists of both a data tree (which contains scripts and pointers to nodes in trees at different locations) and a process, for modelling process interaction, process migration and interaction between processes and data. Our type system is based on types for locations, trees and processes, expressing security levels. The type system enjoys type preservation under reduction (subject reduction). In consequence of subject reduction we prove the following security properties. In a well-typed X-network, data in a location are accessible only to processes in locations of equal or higher security level. Moreover, processes originating in a location can only go to locations of equal or less security level, with the exception of movements which are returns to the “source” location.

We propose a framework in which anonymity protocols are interpreted as particular kinds of channels, and the degree of anonymity provided by the protocol as the converse of the channel’s capacity. We also investigate how the adversary can test the system to try to infer the user’s identity, and we study how his probability of success depends on the characteristics of the channel. We then illustrate how various notions of anonymity can be expressed in this framework, and show the relation with some definitions of probabilistic anonymity in literature.

We present a powerful and flexible method for automatically checking anonymity in a possibilistic general-purpose process algebraic verification toolset. We propose new definitions of a and a , to quantify the precision with which an intruder is able to single out the true originator of a given event or to associate the right event to a given protocol participant. We show how these measures of anonymity can be automatically calculated from a protocol specification in CRL, by using a combination of dedicated tools and existing state-of-the-art CRL tools. To illustrate the flexibility of our method we test the Dining Cryptographers problem and the FOO 92 voting protocol. Our definitions of anonymity provide an accurate picture of the different ways that anonymity can break down, due for instance to coallitions of inside intruders. Our calculations can be performed on a cluster of machines, allowing us to check protocols for large numbers of participants.

We present a simple parametric calculus of processes which exchange mobile code, where type safety is ensured by a combination of static and dynamic checks. That is, internal consistency of each process is locally verified before starting execution, by only relying on type assumptions on missing code; then, at execution time, when locally typechecked code is sent from a process to another, a run-time check based on a subtyping relation ensures that it can be successfully received, without requiring to inspect code again.

The calculus is defined in a parametric way, that is, we do not fix some ingredients which can vary depending on the specific language or system. Notably, we abstract away from the specific nature of the code to be exchanged, and of the static and dynamic checks. We formalize the notion of in our general framework and provide sufficient conditions on the above ingredients which guarantee this property.

We illustrate our approach first on a simple lambda-calculus with records, and then on a calculus of mixin modules which generalizes the previous one.