Translating TLA + to B for Validation with ProB
Translating TLA + to B for Validation with ProB
复制标题
将 TLA 转换为 B 以使用 ProB 进行验证
DOI：
--
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
M. Leuschel
中科院分区：
文献类型：
--
作者：
Dominik Hansen;M. Leuschel
TLA+ 和 B 具有谓词逻辑、算术和集合论的共同基础。然而，仍然存在相当大的差异，例如非常不同的类型和模块化方法。可用的工具支持也存在相当大的差异。在本文中，我们提出了 TLA+ 的非时间部分到 B 的翻译，这使得将 TLA+ 规范输入现有的 B 工具成为可能。该翻译的一部分必须包括类型推断算法，以便生成类型化的 B 规范。还有许多其他棘手的方面，例如翻译模块以及 let/in 和 if/then/else 表达式。我们还将我们的翻译集成到 ProB 中。因此，ProB 为显式状态模型检查器 TLC 提供了补充工具，为 TLA+ 提供方便的动画和约束求解。我们还提供了一系列案例研究，强调了 TLC 的互补性。我们特别强调了在 TLA+ 中解决复杂约束时有时性能上的巨大差异。
TLA+ and B share the common base of predicate logic, arithmetic and set theory. However, there are still considerable differences, such as very different approaches to typing and modularization. There is also considerable difference in the available tool support. In this paper, we present a translation of the non-temporal part of TLA+ to B, which makes it possible to feed TLA+ specifications into existing tools for B. Part of this translation must include a type inference algorithm, in order to produce typed B specifications. There are many other tricky aspects, such as translating modules as well as let/in and if/then/else expressions. We also present an integration of our translation into ProB. ProB thus provides a complementary tool to the explicit state model checker TLC, with convenient animation and constraint solving for TLA+. We also present a series of case studies, highlighting the complementarity to TLC. In particular, we highlight the sometimes dramatic difference in performance when it comes to solving complicated constraints in TLA+.