Translating B to TLA + for Validation with TLC
Translating B to TLA + for Validation with TLC
复制标题
将 B 转换为 TLA 以使用 TLC 进行验证
DOI：
10.1007/978-3-662-43652-3_4
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Michael Leuschel
中科院分区：
文献类型：
--
作者：
Dominik Hansen;Michael Leuschel
基于状态的形式化方法B和TLA+具有谓词逻辑、算术和集合论的共同基础。然而，仍然存在相当大的差异，例如指定状态转换的方式、不同的键入方法以及可用的工具支持。在本文中，我们提出了一种从B totla+到B totla+的转换，以便使用模型检查器TLC验证B规范。该翻译包括许多调整和优化，以允许通过TLC进行有效的检查。此外，我们还提出了一种在公平条件下验证B规格说明的活性性质的方法。我们实现的翻译器Tlc4B自动将B规范转换为TLA+，调用模型检查器TLC，并将结果转换回B。我们使用ProB重新检查TLC生成的反例，并在ProB动画程序中重放它们。Tlc4B还可以将ProB预计算出的常量值传输到TLC。这允许用户结合这两个工具的优势，即ProB的约束求解能力和TLC高度调优的模型检查核心。此外，我们还展示了一种通过在翻译后的TLA+规范中编码证明信息来优化模型检测过程的方法。我们还提供了一系列比较Tlc4Band ProB的案例研究和基准测试。
The state-based formal methods B andTLA+share the common base of predicate logic, arithmetic and set theory. However, there are still considerable differences, such as the way to specify state transitions, the different approaches to typing, and the available tool support. In this paper, we present a translation from B toTLA+so as to validate B specifications using the model checkerTLC. The translation includes many adaptations and optimizations to allow for efficient checking byTLC. Moreover, we present a way to validate liveness properties for B specifications under fairness conditions. Our implemented translator,Tlc4B, automatically translates a B specification toTLA+, invokes the model checkerTLC, and translates the results back to B. We useProBto double check the counter examples produced byTLCand replay them in theProBanimator.Tlc4Bcan also transmit constant values, precalculated byProB, toTLC. This allows the user to combine the strength of both tools, i.e.ProB's constraint solving abilities andTLC's highly tuned model checking core. Furthermore, we demonstrate an approach to optimize the model checking process by encoding proof information in the translatedTLA+specification. We also present a series of case studies and benchmark tests comparingTlc4BandProB.
登录
查看更多内容
将 TLA 转换为 B 以使用 ProB 进行验证
DOI：
--
发表时间：
2012
期刊：
International Conference on Integrated Formal Methods
影响因子：
--
作者：
Dominik Hansen;M. Leuschel
通讯作者：
M. Leuschel
根据正式规范生成测试序列：GSM 11‐11 标准案例研究
DOI：
--
发表时间：
2004
期刊：
Software, Practice & Experience
影响因子：
--
作者：
Eddy Bernard;B. Legeard;Xavier Luck;F. Peureux
通讯作者：
F. Peureux
用于验证 B 模型的 SAL、Kodkod 和 BDD。
DOI：
--
发表时间：
2009
期刊：
影响因子：
--
作者：
Daniel Plagge;M. Leuschel;I. Lopatkin;A. Iliasov;A. Romanovsky
通讯作者：
A. Romanovsky
数字对象标识符 (DOI) 10.1007/s00446-002-0070-8 c ○ Springer-Verlag 2003 Disk Paxos
DOI：
--
发表时间：
2001
期刊：
影响因子：
--
作者：
Steven L. Alter
通讯作者：
Steven L. Alter
Z 2 SALa Z 的基于翻译的模型检查器
DOI：
--
发表时间：
2009
期刊：
影响因子：
--
作者：
J. Derrick;Siobhán North;A. Simons
通讯作者：
A. Simons