Correct Pattern-Based Development Through Refinements and Predicate Transformers

The incremental development of complex systems requires systematic methods to manage scalability and reduce repetitive effort. In formal methods, this incremental process is naturally supported through refinement, where abstract models are gradually enriched with detail. In this paper, we adopt Event-B as the formal method to explore this process. Developing refinements in Event-B often involves repetitive modeling tasks that can become time-consuming and difficult to manage. Patterns help address this by capturing recurring solutions, making refinements more reusable, systematic, and easier to construct while also providing implicit, up-to-date documentation. Building on this, we investigate how patterns could be used to generate Event-B refinements automatically. The patterns proposed in this paper apply a variety of techniques, such as imposing constraints on the model through weakest precondition or strongest postcondition calculus, superposing counters, and introducing various forms of synchronization or observer-based de-synchronization. We also show how the generated model can be automatically simplified to improve its usability and readability, thereby facilitating subsequent refinement steps. Lastly, we demonstrate the effectiveness of our proposed patterns by revisiting two classic case studies.