SAL, Kodkod, and BDDs for Validation of B Models. Lessons and Outlook.

SAL, Kodkod, and BDDs for Validation of B Models. Lessons and Outlook.
复制标题

用于验证 B 模型的 SAL、Kodkod 和 BDD。

DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
A. Romanovsky
A. Romanovsky
中科院分区：
--
文献类型：
--
作者：
Daniel Plagge;M. Leuschel;I. Lopatkin;A. Iliasov;A. Romanovsky

文献摘要

被引文献

相似文献

PROB是基于约束求解的高级B和事件B模型的模型检查器。在本文中，我们研究了替代方法，验证高层次的B模型使用替代技术和工具的基础上使用BDD，SAT解决方案和SMT解决方案。特别是，我们研究是否可以补充，甚至取代使用工具BDDBDDB，Kodkod或SAL。
PROB is a model checker for high-level B and Event-B models based on constraint-solving. In this paper we investigate alternate approaches for validating high-level B models using alternative techniques and tools based on using BDDs, SAT-solving and SMT-solving. In particular, we examine whether PROB can be complemented or even supplanted by using one of the tools BDDBDDB, Kodkod or SAL.