Formal Models for Programming and Composing Correct Distributed Systems
Ludovic Henrio · HAL (Le Centre pour la Communication Scientifique Directe) · 2012
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 languages with a high level of abstraction: active ob jects, algorithmic skeletons, components. To verify correction of the behaviour of an application, I have contributed to the creation of tools for specifying and verifying behavioural distributed applications. My work aims to provide a strong model of programming languages, libraries, and runtime environments provided to the developer, and to guarantee the safe behaviour of distributed applications. During my thesis, I developed the ASP calculus for modelling the behaviour of active ob jects and futures. Since, we created a functional version of this calculus and formalised it in Isabelle/HOL. I also strongly contributed to the definition of a distributed component model - the GCM (Grid Component Model) -, to its formalisation, and to its use for programming adaptive or autonomous components. Finally, I contributed to the specification and behavioural verification of programs based on active ob jects and components, in order to ensure their safe execution. Currently we are working both on a multi-threaded extension of the active ob ject model, better suited for multi-core machine, and on the use of formal methods to design and prove the correction of an algorithm for broadcast on CAN-like peer-to-peer networks (Content Addressable Network). This manuscript provides an overview of all these works.