Z 2 SALa translation-based model checker for Z
Z 2 SALa translation-based model checker for Z
复制标题
Z 2 SALa Z 的基于翻译的模型检查器
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
A. Simons
中科院分区：
文献类型：
--
作者：
J. Derrick;Siobhán North;A. Simons
尽管Z正式规范语言在业界广为人知并被广泛接受，但到目前为止，自动化验证工具还没有很好地支持它，主要是因为在处理语言的抽象方面存在挑战。在本文中，我们讨论了一种为Z构建模型检查器的新方法，它涉及实现从Z到SAL（符号分析实验室的输入语言）的翻译，这是一个包括许多模型检查器和模拟器的工具集。Z2SAL转换处理了许多重要的问题，包括：将无界的抽象规范映射到有界的有限模型，该模型适用于基于bdd的符号检查器；将非建设性和零碎的功能规格说明风格转换为确定性的、基于自动化的规格说明风格；并支持Z数学工具包丰富的基于集合的词汇表。本文讨论了在实现尽可能完整和忠实的翻译方面取得的进展，同时强调了某些假设，尊重某些限制并利用可用的优化。翻译是通过例子来说明的；给出了一个完整的工作实例，并给出了性能数据。
Despite being widely known and accepted in industry, the Z formal specification language has not so far been well supported by automated verification tools, mostly because of the challenges in handling the abstraction of the language. In this paper we discuss a novel approach to building a model-checker for Z, which involves implementing a translation from Z into SAL, the input language for the Symbolic Analysis Laboratory, a toolset which includes a number of model-checkers and a simulator. The Z2SAL translation deals with a number of important issues, including: mapping unbounded, abstract specifications into bounded, finite models amenable to a BDD-based symbolic checker; converting a non-constructive and piecemeal style of functional specification into a deterministic, automaton-based style of specification; and supporting the rich set-based vocabulary of the Z mathematical toolkit. This paper discusses progress made towards implementing as complete and faithful a translation as possible, while highlighting certain assumptions, respecting certain limitations and making use of available optimisations. The translation is illustrated throughout with examples; and a complete working example is presented, together with performance data.