Event-B 机器到 JML 翻译的机器验证证明

Néstor Cataño; Camilo Rueda; Tim Wahls

Event-B 机器到 JML 翻译的机器验证证明

软件工程 2013-09-11 v1 计算机科学中的逻辑编程语言

作者: Néstor Cataño , Camilo Rueda , Tim Wahls

摘要

我们提出了将 Event-B 翻译到 Java 建模语言 (JML) 的机器验证可靠性证明。该翻译基于一个名为 EventB2Jml 的算子，它将 Event-B 事件映射到 JML 方法规范，并将确定性和非确定性赋值映射到 JML 方法后置条件。此翻译此前已作为 EventB2Jml 工具实现。我们在形式化证明中采用了“自食其果”的方法，即在 Event-B 中对 Event-B 和 JML 进行形式化，并使用 Rodin 平台完成证明验证。因此，对于任何 Event-B 替换（无论是事件还是赋值）以及通过应用 EventB2Jml 于该替换所获得的 JML 方法规范，我们证明了 JML 方法规范的语义由该替换的语义所模拟。因此，从 Event-B 替换翻译得到的 JML 规范是该替换的一个精化。我们的证明包含不变量和标准的 Event-B 初始化事件，但不包括完整的机器或 Event-B 上下文。我们假设 JML 和 Event-B 的语义均在相同的初始和最终状态下运行，并论证了这一假设的合理性。

关键词

机器验证证明 Event-B Java 建模语言形式化验证翻译可靠性 Rodin 平台精化

引用

@article{arxiv.1309.2339,
  title  = {A Machine-Checked Proof for a Translation of Event-B Machines to JML},
  author = {Néstor Cataño and Camilo Rueda and Tim Wahls},
  journal= {arXiv preprint arXiv:1309.2339},
  year   = {2013}
}

备注

26 pages

Event-B 机器到 JML 翻译的机器验证证明

摘要

关键词

引用

备注

相关论文