Integration of Automatic Theorem Provers in Event-B Patterns

Abstract

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 we 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.