文章基本信息

标题：Integration of Automatic Theorem Provers in Event-B Patterns
本地全文：下载
作者：Eman Elsayed ; Gaber El-Sharawy ; Enas El-Sharawy 等
期刊名称：International Journal of Software Engineering & Applications (IJSEA)
印刷版ISSN：0976-2221
电子版ISSN：0975-9018
出版年度：2013
卷号：4
期号：1
页码：29
出版社：Academy & Industry Research Collaboration Center (AIRCC)
摘要：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.
关键词：Formal methods; Event-B; Design patterns; SMT-Solver; Refinement