Seven at one stroke: LTL model checking for high-level specifications in B, Z, CSP, and more
Seven at one stroke: LTL model checking for high-level specifications in B, Z, CSP, and more
复制标题
一举七动：LTL 模型检查 B、Z、CSP 等高级规格
DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
M. Leuschel
中科院分区：
文献类型：
--
作者：
Daniel Plagge;M. Leuschel
形式模型的大小正在稳步增加，工业用户要求能够使用可表达的时态查询语言来验证和探索高级形式规范。我们提出了一种扩展的LTL，它非常适合于验证B、Z和CSP规范。我们提出了一个在PROB工具中实现的通用的、灵活的LTL模型检查器，它可以应用于多种形式化方法，如B、Z、CSP、B||CSP以及对象Petri网、补偿CSP和DSL。我们的算法可以处理死锁状态、部分搜索的状态空间、过去的算子，并且可以与已有的PROB对称性约简技术相结合。我们从总体上证明了算法的正确性，并结合对称性约简进行了验证。最后，我们给出了我们的工具的各种应用和实证结果，表明该工具可以在实践中成功地应用。
The size of formal models is steadily increasing and there is a demand from industrial users to be able to use expressive temporal query languages for validating and exploring high-level formal specifications. We present an extension of LTL, which is well adapted for validating B, Z and CSP specifications. We present a generic, flexible LTL model checker, implemented inside the PROB tool, that can be applied to a multitude of formalisms such as B, Z, CSP, B||CSP, as well as Object Petri nets, compensating CSP, and dSL. Our algorithm can deal with deadlock states, partially explored state spaces, past operators, and can be combined with existing symmetry reduction techniques of PROB. We establish correctness of our algorithm in general, as well as combined with symmetry reduction. Finally, we present various applications and empirical results of our tool, showing that it can be applied successfully in practice.
DOI：
10.1007/978-3-642-28756-5_47
发表时间：
2012
期刊：
--
影响因子：
--
作者：
Basler G
通讯作者：
Basler G