Integration of Automatic Theorem Provers in Event-B Patterns
Event-B is a formal method for the system level modeling and analysis of dependable applications. It is supported by an open and extendable Eclipse-based tool set called Rodin. In this paper, the authors proposed using automatic theorem provers known as SMT-solvers with event-B pattern. The benefits of that are to reduce the proving effort, to reuse a model and to increase the degree of automation. The proposed approach has been applied successfully on two different case studies.