BEval：利用当前验证技术扩展 Atelier B 的插件
软件工程
2014-01-07 v1 计算机科学中的逻辑
摘要
本文介绍了 BEval，它是 Atelier B 的一个扩展，旨在提高 B 方法或 Event-B 中验证活动的自动化程度。它结合了用于管理和验证软件项目的工具（Atelier B）与模型检测器/动画器（ProB），使得前者生成的验证条件可由后者进行评估。在我们的实验中，两种主要的验证策略（手动和自动）均显示出显著改进，因为 ProB 的评估器证明了其对 Atelier B 内置证明器的互补性。我们使用微控制器指令集的 B 模型进行了实验；若干无法通过 Atelier B 的证明器自动或手动解除的验证条件，在使用 BEval 时得到了自动验证。
引用
@article{arxiv.1401.0972,
title = {BEval: A Plug-in to Extend Atelier B with Current Verification Technologies},
author = {Valério Medeiros and David Déharbe},
journal= {arXiv preprint arXiv:1401.0972},
year = {2014}
}
备注
In Proceedings LAFM 2013, arXiv:1401.0564