Faithful Translations among Models and Specifications

摘要

Numerous translations exist between the design notations of formal methods tools, usually between two specific notations. In addition, more general translation frameworks are under development. For any translation it is vital that properties true of the semantic interpretations of the source and the translated notations are closely related. Some possible applications of translations among model descriptions are described and key issues in translating among models with inconsistent features are identified, leading to a source and a target model that do not always preserve the correctness of properties in a simple way. The concept is presented of a faithful relation among models and families of properties true of those models. In this framework families of properties are provided with uniform syntactic transformations, in addition to the translations of the models. Three variants are presented, depending on the intended use of the translation, so that the correctness of a property in a model corresponds to the correctness of the transformed property in the translated model. This framework is shown appropriate for common instances of relations among translations previously treated in an ad hoc way. Furthermore, it allows expressing connections among models where one is neither a refinement nor an abstraction of the other. The classes of properties that can be faithful for a given translation provide a measure of the usefulness of the translation.