Abstract Data Types in Event-B - An Application of Generic Instantiation

Abstract. Integrating formal methods into industrial practice is a chal-lenging task. Often, different kinds of expertise are required within the same development. On the one hand, there are domain engineers who have specific knowledge of the system under development. On the other hand, there are formal methods experts who have experience in rigor-ously specifying and reasoning about formal systems. Coordination be-tween these groups is important for taking advantage of their expertise. In this paper, we describe our approach of using generic instantiation to facilitate this coordination. In particular, generic instantiation enables a separation of concerns between the different parties involved in develop-ing formal systems.