Rationale for using CIF to CIF transformationsΒΆ

One of the goals of the Compositional Interchange Format for hybrid systems (CIF) is to establish interoperability among a wide range of formalisms (and tools) by means of model interchange. That is, we want to allow interchange of models in different languages, by using transformations from or to the CIF. An example of such a transformation could be to transform a CIF specification to UPPAAL, to allow verification using of CIF specifications using the UPPAAL model checker.

Languages are different by nature, and often not all concepts of a language can be translated to all other languages. It is quite common that a feature of the source language of the transformation can not be translated to the target language, or that it is difficult to translate it directly. Therefore, each transformation defines a subset of the input (source) language that the transformation accepts.

First, the subsets of both languages that correspond ‘easily’ are identified. Concepts that are directly transformable are those concepts that exist in both languages and have similar semantics. Often, concepts such as variables, arithmetic operators, and literals are the same in the source and target languages. The next step is to create a cross-formalism model transformation between these subsets, and vice versa (if the transformation is to be bi-directional). Once this transformation is defined, it is possible to translate models within the subset of the source language, to the target language. The subset of the source language that corresponds ‘easily’ is usually kept rather small, and only contains those concepts that closely map related concepts of the target language. This ensures that the cross-formalism transformation is kept simple, understandable, and manageable. This is essential for cross-formalism transformations, as they are inherently complex due to the influence of syntax and semantics of not one, but two languages.

Due to the rather small source subset, the practical use of the cross-formalism transformation is seriously reduced. To remedy this situation, one can employ transformations within the source language, to translate certain subsets of the source language into other subsets of that same source language.

Obviously, within-formalism transformations should be semantics preserving. That is, the specification that results from a transformation should have the same behavior as the original specification. Formally, transformations should ensure that the source and target specifications are equivalent, using some form of bisimilarity.

If one defines such within-formalism transformations (that is, CIF to CIF transformations) in a general and reusable fashion, they can be easily reused to broaden the translatable subset of not only the transformation between formalism A and formalism B, but also for the transformation between formalism A and a third formalism C, assuming the transformations between A and B and between A and C have similar source subsets, which is quite common. This type of reuse can be further extended by splitting the within-formalism transformations into multiple within-formalism transformations, if they are orthogonal.

We can conclude that there are several major advantages to our approach to model interchange. The first is that we keep our cross-formalism transformations simple. This usually increases our confidence in their correctness, and also makes formal proofs less tedious. Secondly, it also separates concerns, by separating the actual cross-formalism transformation from the within-formalism transformation. Thirdly, the separation allows for easy reuse, and reduces the implementation effort of future cross-formalism transformations.