Automatic Generation of an Operational CSP-Z Specification from an Abstract Temporal^Z Specification

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 T_emporalZ 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 T_emporalZ 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 T_emporalZ with the F_orMAAD method.