%0 Journal Article
%T Integration of Automatic Theorem Provers in Event-B Patterns
%A Eman Elsayed
%A Gaber El-Sharawy
%A Enas El-Sharawy
%J International Journal of Software Engineering & Applications
%D 2013
%I Academy & Industry Research Collaboration Center (AIRCC)
%X Event-B is a formal method for the system level modeling and analysis of dependable applications. It issupported by an open and extendable Eclipse-based tool set called Rodin. In this paper we proposed usingAutomatic theorem provers known as SMT-solvers with event-B pattern. The benefits of that are to reducethe proving effort, to reuse a model and to increase the degree of automation. The proposed approach hasbeen applied successfully on two different case studies.
%K Formal methods
%K Event-B
%K Design patterns
%K SMT-Solver
%K Refinement
%U http://airccse.org/journal/ijsea/papers/4113ijsea03.pdf