IBM Logo
IBM Research Lab in Haifa
Hot Shots  
FV Research in HRL  

Download the presentation

Shmuel Katz



Faithful Translations Among Models and Specifications in VeriTech

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.)