HENRIO , Ludovic

My research focuses on distributed programming models, more precisely using ob jects and components. In this area, I provided tools easing the programming of large-scale distributed applications and verifying their correct behaviour. To facilitate the programming of distributed applications, I contributed to the design and the development of...

The objective of this thesis is to design an object calculus that allows one to write parallel and distributed applications, particularly on wide range networks, while ensuring good properties. This calculus is named ASP : Asynchronous Sequential Processes. The main characteristics of ASP are: asynchronous communications, futures, and a...

No description

Among the programming models for parallel and distributed computing, one can identify two important families. The programming models adapted to data-parallelism, where a set of coordinated processes perform a computation by splitting the input data; and coordination languages able to express complex coordination patterns and rich interactions...

This paper presents a brief overview of our efforts in the behavioural specification and verification of distributed component systems. Our objective in this work is to provide tools to help the programmer specify the behaviour of his/her components, generate a model, and check the correctness of his/her application.

Group-based distributed systems are specific cases of distributed applications with a parameterized topology. They are naturally modelled by systems with a very large state space. We encode the behavioural semantics of group-based applications using the intermediate format FIACRE. We have experimented with model-checking of such systems, using...

In this paper we present a formalization of Abadi's and Cardelli's theory of ob jects in the interactive theorem prover Isabelle/HOL. Our motivation is to build a mechanized HOL-framework for the analysis of a functional calculus for distributed ob jects. In particular, we present (a) a formal model of ob jects and its operational semantics...

In order to tackle the development of concurrent and distributed systems, the active object programming model provides a high-level abstraction to program concurrent behaviours. There exists already a variety of active object frameworks targeted at a large range of application domains: modelling, verification, efficient execution. However,...

This paper provides a sound foundation for autonomous objects communicating by remote method invocations and futures. As a distributed extension of sigma-calculus, we define aspfun, a calculus of functional objects, behaving autonomously and communicating by a request-reply mechanism: requests are method calls handled asynchronously and futures...

Futures enable an efficient and easy to use programming paradigm for distributed applications. A natural way to benefit from distribution is to perform asynchronous invocations to methods or services. Upon invocation, a request is en-queued at the destination side and the caller can continue its execution. But a question remains: ``what if one...

No description

Formal reasoning on Peer-to-Peer (P2P) systems is an intimidating task. This paper focuses on broadcast algorithms for Content Addressable Network (CAN). Since these algorithms run on top of complex P2P systems, finding the right level of abstraction in order to prove their functional correctness is difficult. This paper presents a mechanized...

The various algorithms underlying P2P systems are notoriously difficult to design and analyze. Coming up with new proven algorithms for such large scale systems is a challenging task. We report on the initial steps of an ongoing work that aims to devise an efficient correct-by-construction broadcast algorithm for the CAN structured overlay...

Based on the imp sigma-calculus, ASP (Asynchronous Sequential Processes) defines distributed applications behaving deterministically. This article extends ASP by building hierarchical and asynchronous distributed components. Components are hierarchical - a composite can be built from other components, and distributed - a composite can span over...

National audience

This document presents an object language that allows one to program parallel and distributed applications that behave in a deterministic manner, even if they are distributed over local or wide area networks. An object calculus, Asynchronous Sequential Processes, is proposed and determinism properties are proposed. ASP main characteristics are...

In an Infrastructure As A Service (IaaS) cloud, the scheduler deploys VMs to servers according to service level objectives (SLOs). Clients and service providers must both trust the infrastructure. In particular they must be sure that the VM scheduler takes decisions that are consistent with its advertised behaviour. The difficulties to master...

ABS is an object-oriented modeling language that is based on a concurrent object group model, derived itself from the active object model. Its goal is to describe distributed and concurrent applications in order to verify their properties and make them safer. Thanks to the ABS Tool Suite, ABS programs can be translated into the Java programming...

This paper presents a novel way to introduce self-configuration and self-optimization autonomic characteristics to algorithmic skeletons using event driven programming techniques. Based on an algorithmic skeleton language, we show that the use of events greatly improves the estimation of the remaining computation time for skeleton execution....