An Event-B Development Process for the Distributed BIP Framework.

We present a refinement-based methodology to design correct by construction distributed systems specified as Event-B models. Starting from an Event-B machine, the studied process proposes successive steps in order to split and schedule the computation of complex events and then to map them on subcomponents. The specification of these steps is done through two domain specific languages. From these specifications, two refinements are generated. Eventually, a distributed code architecture is also generated. The correctness of the process relies on the correctness of the refinements and the translation. We target the distributed BIP framework.