  Event-B is a refinement-based formal method that has been shown to be useful
in developing concurrent and distributed programs. Large models can be
decomposed into sub-models that can be refined semi-independently and executed
in parallel. In this paper, we show how to introduce explicit control flow for
the concurrent sub-models in the form of event schedules. We explore how
schedules can be designed so that their application results in a
correctness-preserving refinement step. For practical application, two patterns
for schedule introduction are provided, together with their associated proof
obligations. We demonstrate our method by applying it on the dining
philosophers problem.
