Correct Pattern-Based Development Through Refinements and Weakest Preconditions Calculus

This paper focuses on the preliminary steps of developing safety-critical systems. We investigate how patterns could be used to generate Event-B refinements automatically. The patterns proposed in this paper either impose constraints on the model through weakest precondition calculus, superpose counters, or introduce de-synchronization mechanisms using observers. We show how the weakest precondition calculus integrated into the patterns can be simplified and become usable. Moreover, for our patterns to be fully usable in subsequent refinement steps, we produce as much as possible readable Event-B models. Finally, we revisit a classic case study using our proposed patterns.