Event-B 模型的自动化验证
软件工程
2016-11-10 v1
摘要
Event-B 是基于模型、证明驱动的规范中最流行的符号之一。它提供了一种基于一阶逻辑(FOL)和 ZF 集合论的相对高级的数学语言，以及一种简洁而富有表现力的建模符号。模型正确性通过证明（消解）若干由模式条件的语法实例化构建的猜想来确立。大量可证明的猜想需要用户提供证明提示。对于较大的模型，这变得极其繁重，因为相同或相似的证明必须反复重复，尤其是在模型重构阶段之后。在本文中，我们简要介绍了一种基于 Why3 伞式证明器的新型 Rodin 平台证明后端。
引用
@article{arxiv.1611.02923,
title = {Automating Verification of Event-B Models},
author = {Paulius Stankaitis and Alexei Iliasov and David Adjepon-Yamoah and Alexander Romanovsky},
journal= {arXiv preprint arXiv:1611.02923},
year = {2016}
}
备注
Event-B day 2016, Tokyo