Numerous translations exist between the design notations of formal
methods tools, usually between two specific notations.
VeriTech is a general framework for translating among formal
verification tools. The notation of each component tool
is translated to a core representation, and the core is translated
to each component.
For any translation, whether direct or through an
intermediate notation, it is crucial that
the properties true of the semantic interpretations of the source
and the translated notations are closely related.
Key issues in translating among models with inconsistent
features are described, leading to models that are closely related,
but that do not always preserve either the structure or the correctness of
properties in a simple way. We define a `faithful' relation among
models and families of properties true of those models. In this
context, families of properties are provided with uniform
transformations, in conjunction with the translations of the models.
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 talk describes joint work with Orna Grumberg.)