The Theory and Practice of Translating Models and Properties
<P>
 Speaker: Shmuel Katz
          Computer Science Department
          The Technion
 
<P>
 Abstract:
 The motivation for translating a description of a model in one formal
methods notation into another is reviewed, and the VeriTech framework
for translation is described. A system being analyzed is seen as a 
collection of versions, along with a characterization of how the 
versions are related, and properties known to be true of each version. 
The reasons that translations cannot always be exact are analyzed.

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.
This framework is shown appropriate for common instances of relations 
among translations previously treated in an ad hoc way. The classes of
properties that can be faithful for a given translation provide a 
measure of the usefulness of the translation.
Validation of the semantic assumptions made about the translation
is achieved by generating proof obligations for each activation of the
associated compiler, generalizing previous work on compiler validation.