Jump to : Download | Abstract | Keywords | Contact | BibTex reference | EndNote reference |


Rouwaida Abdallah. Implementability of distributed systems described with scenarios. PhD Thesis École normale supérieure de Cachan - ENS Cachan, July 2013.

Download [help]

Download Hal paper: Hal : Hyper Archive en ligne

Download paper: Adobe portable document (pdf) pdf

Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
This page is automatically generated by bib2html v216, © INRIA 2002-2007, Projet Lagadic


{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 information before resending them. We then propose a new technique that we named "localization" to transform an arbitrary HMSC specification into a local HMSC, hence allowing correct synthesis. We show that this transformation can be automated as a constraint optimization problem. The impact of modifications brought to the original specification can be minimized with respect to a cost function. Finally, we have implemented the synthesis and the localization approaches into an existing tool named SOFAT. We have, in addition, implemented to SOFAT the automatic code generation of a Promela code and a JAVA code for REST based web services from HMSCs.}


[ Code generating ] [ Synthesis ] [ Distributed systems ] [ Cfsm ] [ Hmsc ]

BibTex Reference

   Author = {Abdallah, Rouwaida},
   Title = {{Implementability of distributed systems described with scenarios}},
   School = {École normale supérieure de Cachan - ENS Cachan},
   Month = {July},
   Year = {2013}

EndNote Reference [help]

Get EndNote Reference (.ref)