将Event-B编码为Alloy进行模型检验
摘要：使用SAT-based模型发现器的基于事件B（Event-B）和Alloy是两种基于相当不同方法论的形式化规范语言。Event-B使用定理证明器来证明给定规范中的不变式是否成立，而Alloy使用基于SAT的模型发现器。在某些情况下，Event-B不变式可能无法自动证明，因此需要进行常常困难的交互式证明。解决这个问题的一种方法是使用模型检查来验证不变式。本研究研究了将Event-B机器和上下文编码为Alloy，以便使用Alloy的SAT-based引擎进行时态模型检查的方法。
作者：Paulo J. Matos, Joao Marques-Silva
论文ID：0805.3256
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2008-05-30