An Event-B Development Process for the Distributed BIP Framework

Abstract

We present a refinement-based methodology to design correct by construction distributed systems specified as Event-B models. Our approach makes explicit the transition from formal requirements to a distributed executable model. Starting from an Event-B machine, we propose 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.