检查形式化方法工具的计算结果——ProB 的二级工具链
软件工程
2014-04-29 v1 计算机科学中的逻辑
编程语言
摘要
我们介绍了 pyB 的实现，这是一个针对 B 语言的谓词和表达式检查器。该工具旨在作为数据验证和数据生成的二级工具链使用，而 ProB 则用于主工具链。事实上，pyB 是一个独立的净室实现（cleanroom-implementation），用于双重检查由 ProB（一种 B 规范的动画器和模型检查器）生成的解决方案。主要目标之一是联合使用 ProB 和 pyB，为高完整性安全关键应用生成可靠的输出。尽管 pyB 仍在开发中，但 ProB/pyB 工具链已在各种工业 B 机器和数据验证任务中成功测试。
引用
@article{arxiv.1404.6609,
title = {Checking Computations of Formal Method Tools - A Secondary Toolchain for ProB},
author = {John Witulski and Michael Leuschel},
journal= {arXiv preprint arXiv:1404.6609},
year = {2014}
}
备注
In Proceedings F-IDE 2014, arXiv:1404.5785