AbstractsComputer Science

Les systèmes distribués sont au cœur de nombreuses applications modernes (réseaux sociaux, services web, etc.). Cependant, les développeurs sont confrontés à de nombreux défis dans l’implémentation des systèmes distribués, notamment les comportements erronés à éviter et qui sont causées par la concurrence entre les entités de ce système. La génération automatique de code à partir des exigences des systèmes distribués reste un vieux rêve. Dans cette thèse, nous considérons la génération automatique d'un squelette de code portant sur les interactions entre les différentes entités d'un système distribué. Cela nous permet d'éviter les comportements erronés causés par la concurrence. Ensuite, ce squelette peut être complété par l'ajout et le débogage du code qui décrit les actions locales qui se passent sur chaque entité indépendamment de ses interactions avec les autres entités. Distributed systems lie at the heart of many modern applications (social networks, web services, etc.). However, developers face many challenges in implementing distributed systems. The major one we focus on is avoiding the erroneous behaviors, that do not appear in the requirements of the distributed system, and that are caused by the concurrency between the entities of this system. The automatic code generation from requirements of distributed systems remains an old dream. In this thesis, we consider the automatic generation of a skeleton of code covering the interactions between the entities of a distributed system. This allows us to avoid the erroneous behaviors caused by the concurrency. Then, in a later step, this skeleton can be completed by adding and debugging the code that describes the local actions happening on each entity independently from its interactions with the other entities. The automatic generation that we consider is from a scenario-based specification that formally describes the interactions within informal requirements of a distributed system. We choose High-level Message Sequence Charts (HMSCs for short) as a scenario-based specification for the many advantages that they present: namely the clear graphical and textual representations, and the formal semantics. The code generation from HMSCs requires an intermediate step, called “Synthesis” which is their transformation into an abstract machine model that describes the local views of the interactions by each entity (A machine representing an entity defines sequences of messages sending and reception). Then, from the abstract machine model, the skeleton’s code generation becomes an easy task. A very intuitive abstract machine model for the synthesis of HMSCs is the Communicating Finite State Machine (CFSMs). However, the synthesis from HMSCs into CFSMs may produce programs with more behaviors than described in the specifications in general. We thus restrict then our specifications to a sub-class of HMSCs named "local HMSC". We show that for any local HMSC, behaviors can be preserved by addition of communication controllers that intercept messages to add stamping…