Automatic Generation of an Operational CSP-Z Specification from an Abstract Temporal^Z Specification
Automatic Generation of an Operational CSP-Z Specification from an Abstract Temporal^Z Specification
复制标题
DOI：
10.1109/compsacw.2012.53
复制
发表时间：
2012-07
期刊：
影响因子：
--
通讯作者：
Thouraya Gouasmi;Amira Regayeg;A. Kacem
中科院分区：
文献类型：
--
作者：
Thouraya Gouasmi;Amira Regayeg;A. Kacem
形式化方法在开发分布式系统时非常有用，特别是在开发关键应用程序时。在这种情况下，这项工作的目的是为了解决抽象设计语言和它们的实现之间的差距，定义一个自动翻译从一个抽象的正式规范使用TemporalZ到一个操作规范使用CSP-Z。我们的目标在于，首先，通过定义一系列翻译规则，从Z规范生成CSP-Z规范。其次，我们建议这些规则的扩展，以考虑到特定的概念，一个TemporalZ规范的Z和LTL的集成。这种转换由ANTLR工具支持和实现。最后，我们说明了这项工作，通过翻译一个空中交通管制系统，这是指定在TemporalZ与ForMAAD方法。
Formal methods can be useful in developing distributed systems, in particular when critical applications are being developed. In this context, the purpose of this work is to define an automatic translation from an abstract formal specification using TemporalZ into an operational specification using CSP-Z in order to address the gap between the abstract design languages and their implementation. Our objective consists in, first, to generate a CSP-Z specification from a Z specification by defining a list of translation rules. Second, we suggest an extension of these rules in order to take into consideration the specific concepts of a TemporalZ specification as an integration of Z and LTL. This translation is supported and implemented by the ANTLR tool. Finally, we illustrate this work by translating an air traffic control system which is specified in TemporalZ with the ForMAAD method.