MADELAINE , Eric

Since 2001, in the Oasis team, I have developed research on the semantics of applications based on distributed objects, applying in the context of a real language, and applications of realistic size, my previous researches in the field of process algebras. The various aspects of this work naturally include behavioral semantics and the...

International audience

Component-based software emerged as a promising paradigm to deal with the ever increasing need for mastering systems' complexity, for enabling evolution and reuse, and for driving software engineering into sound production and engineering standards. Soon, however, it became a popular technology long before well understood and widely adopted...

Parameterised Networks of Synchronised Automata (pNets) is a machine-oriented semantic formalism used for specifying and verifying the behaviour of distributed components or systems. In addition, it can be used to define the semantics of languages in the parallel and distributed computation area. Unlike other traditional process calculi, pNets...

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.

Nous étudions les méthodes de preuve des propriétés comportementales d'applications Java distribuées dans lesquelles les objets sur des sites différents coopèrent par appels distants de méthodes. La bibliothèque ProActive fournit un moyen simple et efficace pour mettre en oeuvre cette coopération par définition de primitives qui facilitent la...

International audience

We present a case study describing the formal specification and verification of the Chilean electronic invoice system, which has been defined by the Chilean taxes administration. The system is described by graphical specifications consisting of labelled transition systems, composed using synchronisation networks. Both, transition systems and...

本文为分布式语言提出一个表达能力较强的模型-同步自动机的参数化网络。 通过定义开放式自动机给出了此模型的行为语义, 并在此基础上给出了一种特殊的等价关系--规范假设互模拟等价。 我们讨论了这种等价关系在规范假设条件下的可复合性和可判定性。

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...

Component-based Engineering aims at providing a modular means to specify a wide range of applications. The idea is to promote a clean separation of concerns, and thus reusability, in order to ease the burden of software development and maintenance. The specification of such component models however, tends to be informal, leaving their inherent...

Open Automata (OA) are symbolic and parameterized models for open concurrent systems. Here open means partially specified systems, that can be instantiated or assembled to build bigger systems. An important property for such systems is "compositionality", meaning that logical properties, and equivalences, can be checked locally, and will be...

Distributed Java applications use remote method invocation as a communication means between distributed objects. The ProActive library provides high level primitives and strong semantic guarantees for programming Java applications with distributed, mobile, secured components. We present a method for building finite, parameterized models...

We present a novel specification language called JDC to be used at design phase of distributed components. The extensive seek for asynchrony in distributed components demands new techniques for its specification that have not been addressed before. We propose to focus the specification on its data-flow; this allows to reason about...

Distributed Java applications use remote method invocation as a communication means between distributed objects. The ProActive library provides high level primitives and strong semantic guarantees for programming Java applications with distributed, mobile, secured components. We present a method for building finite, parameterized models...

Components allow to design applications in a modular way by enforcing a strong separation of concerns. In distributed systems this separation of concerns have to be composed with distribution of controls due to asynchrony. This article relies on Fractive, an implementation of the Fractal component model allowing to unify the notion of...

Architecture Description Languages (ADL) provide descriptions of a software system in terms of its structure. Such descriptions give a high-level overview and come from the need to cope with arbitrarily complex dependencies arising from software components.In this paper we present Painless, a novel ADL with a declarative trait supporting...

We describe a method for the specification and verification of the dynamic behaviour of component systems. Building applications using a component framework allows the developers to specify the architecture, the deployment, the life-cycle of the system with well-defined formalisms, and to gain productivity by reusing existing components. But...

The 11th Theoretical Aspects of Software Engineering Conference (TASE 2017) will be held in Nice, France on September 13-15, 2017. TASE is an international symposium that aims to bring together researchers and developers from academia and industry with interest in the theoretical aspects of software engineering. Modern society is increasingly...

Live-migration has become a common operation on virtualized infrastructures. Indeed, it is widely used by resource management algorithms to distribute the load between servers and to reduce energy consumption. Operators rely also on migrations to prepare production servers for critical maintenance by relocating their running VMs elsewhere. To...

We provide a solution for the design of safe concurrent systems by compositional application of verified design patterns-called ar-chitectures-to a small set of functional components. To this end, we extend the theory of architectures developed previously for the BIP framework with the elements necessary for handling data: definition and...

We present the complete process of a formal specification and verification of the Chilean electronic invoice system which has been defined by the tax agency. We use this case study as a real-world and real-size example to illustrate our methodology for specification and verification of distributed applications. Our approach is based on a new...

The modularity offered by component-based systems made it one of the most employed paradigms in software engineering. Precise structural specification is a key ingredient that enables their verification and consequently their reliability. This gains special relevance for reconfigurable component-based systems. To this end, the Grid Component...

In a virtualized data center, server maintenance is a common but still critical operation. A prerequisite is indeed to relocate elsewhere the Virtual Machines (VMs) running on the production servers to prepare them for the maintenance. When the maintenance focuses several servers, this may lead to a costly relocation of several VMs so the...

In this paper, we provide a theory for the operators composing concurrent processes. Open pNets (parameterised networks of synchronised automata) are new semantic objects that we propose for defining the semantics of composition operators. This paper defines the operational semantics of open pNets, using "open transitions" that include symbolic...