Abstract Data Types in Event-B - An Application of Generic Instantiation
This addresses the problem of coordination in formal system development for industrial practitioners, but it appears incremental as it applies an existing technique to a specific context.
The paper tackles the challenge of integrating formal methods into industrial practice by proposing the use of generic instantiation to separate concerns between domain engineers and formal methods experts, facilitating coordination and leveraging their expertise.
Integrating formal methods into industrial practice is a challenging 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 rigorously specifying and reasoning about formal systems. Coordination between 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 developing formal systems.