Duration: 35:01

108 views

2

Although distributed systems are widely used nowadays, their implementation and deployment is still a time-consuming, error-prone, and hardly predictive task. In this talk, I will present a methodology for producing automatically efficient and correct-by-construction distributed implementations by starting from a high-level model of the application software in BIP. BIP (Behavior, Interaction, Priority) is a component-based framework with formal semantics that rely on multi-party interactions for synchronizing components and dynamic priorities for scheduling between interactions. Our methodology transforms arbitrary BIP models into Send/Receive BIP models, directly implementable on distributed execution platforms. The transformation consists of (1) breaking the atomicity of actions in atomic components by replacing strong synchronizations with asynchronous Send/Receive interactions; (2) inserting several distributed controllers that coordinate the execution of interactions according to a user-defined assignment of interactions to controllers, and (3) augmenting the model with a distributed algorithm for handling distributed conflicts between controllers. The obtained Send/Receive BIP models are proven observationally equivalent to their corresponding initial models. Hence, all functional properties of the initial high-level model are preserved by construction in the implementation. Moreover, Send/Receive BIP models can be used to automatically derive distributed implementations. Currently, it is possible to generate distributed C++ implementations using (1) TCP sockets for conventional communication, (2) MPI primitives for multi-processor platforms, and (3) POSIX Threads for deployment on multi-core platforms. This method is fully implemented. I will present concrete results obtained under different scenarios (i.e., partitioning of interactions and choice of algorithm for distributed conflict resolution) and case various case studies.