BEval：一个用当前验证技术扩展Atelier B的插件
BEval: A Plug-in to Extend Atelier B with Current Verification Technologies
摘要：
本文介绍了BEval，Atelier B的扩展，以提高B方法或Event-B中验证活动的自动化程度。它结合了管理和验证软件项目的工具（Atelier B）和模型检查器/动画（ProB），以便用后者评估前者生成的验证条件。在我们的实验中，两个主要的验证策略（手动和自动）显示出显着的改善，ProB的评估证明补充工作室B内置的证明。我们使用微控制器指令集的B模型进行了实验;使用BEval自动验证了我们无法使用AtelierB的校准器自动或手动放电的几个验证条件。
英文摘要：
This paper presents BEval, an extension of Atelier B to improve automation in the verification activities in the B method or Event-B. It combines a tool for managing and verifying software projects (Atelier B) and a model checker/animator (ProB) so that the verification conditions generated in the former are evaluated with the latter. In our experiments, the two main verification strategies (manual and automatic) showed significant improvement as ProB's evaluator proves complementary to Atelier B built-in provers. We conducted experiments with the B model of a micro-controller instruction set; several verification conditions, that we were not able to discharge automatically or manually with AtelierB's provers, were automatically verified using BEval.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
