CTL
28 October 2010 - 13h30
Centralized and Distributed Implementations of Correct-by-construction Component-based Systems by using Source-to-source Transformations in BIP (Phd Defense)
by Mohamad Jaber from VERIMAG
Abstract: The thesis studies theory and methods for generating automatically centralized and distributed implementations from a high-level model of an application software in BIP. BIP (Behavior, Interaction, Priority) is a component framework with formal operational semantics. Coordination between components is achieved by using multiparty interactions and dynamic priorities for scheduling interactions.
A key idea is to use a set of correct source-to-source transformations preserving the functional properties of a given application software. By application of these transformations we can generate a full range of implementations from centralized to fully distributed.
Centralized Implementation:
the implementation method transforms the interactions of an application software described in BIP and generates a functionally equivalent program. The method is based on the successive application of three types of source-to-source transformations: flattening of components, flattening of connectors and composition of atomic components. We show that the system of the transformations is confluent and terminates. By exhaustive application of the transformations, any BIP component can be transformed into an equivalent monolithic component. From this component, efficient standalone C++ code can be generated.
Distributed Implementation:
the implementation method transforms an application software described in BIP for a given partition of its interactions, into a Send/Receive BIP model. Send/Receive BIP models consist of components coordinated by using asynchronous message passing (Send/Receive primitives). The method leads to 3-layer architectures. The bottom layer includes the components of the application software where atomic strong synchronization is implemented by sequences of Send/Receive primitives. The second layer includes a set of interaction protocols. Each protocol handles the interactions of a class of the given partition. The third layer implements a conflict resolution protocol used to resolve conflicts between conflicting interactions of the second layer.
Depending on the given partition, the execution of obtained Send/Receive BIP model range from centralized (all interactions in the same class) to fully distributed (each class has a single interaction).
From Send/Receive BIP models and a given mapping of their components on a platform providing Send/Receive primitives, an implementation is automatically generated. For each class of the partition we generate C++ code implementing the global behavior of its components.
The transformations have been fully implemented and integrated into BIP tool-set. The experimental results on non trivial examples and case studies show the novelty and the efficiency of our approach.
Jury:
Président: Jean-Bernard STEFANI (INRIA, Grenoble, France).
Rapporteurs: Janos SZTIPANOVITS (Vanderbilt University, Nashville, USA).
Michel RAYNAL (IRISA, Rennes, France).
Examinateurs: Jean-Paul BODEVEIX (IRIT, Toulouse, France).
Directeurs de thèse: Joseph SIFAKIS (CNRS, Verimag Laboratory, France).
Jean-Claude FERNANDEZ (UJF, Verimag Laboratory, France).
