Pattern-Based Refinement Generation Through Domain Specific Languages

The Event-B method is generally used to build models incrementally by integrating high level requirements. However, developing correct systems is not a cakewalk and remains a challenging task. In this paper, we focus on the preliminary steps of the development of safety-critical systems. We investigate how patterns could be used to generate refinements automatically in the context of an Event-B development. Our main concerns are first to simplify the development of such systems by the use of patterns, and second to produce Event-B machines such that the user can choose to refine them additionally.