A Framework for Translating Models and Specifications |
| The reasons for translating a description of a model in one notation
into another are reviewed. This includes both translating entire models
and describing different aspects of a system using different notations.
Some examples are presented that show new ways of dividing a problem into
part proven with model checking and part proven using theorem proving.
In order to demonstrate the ideas, the VeriTech framework for translation is described. A system being analyzed is seen as a collection of versions, along with a description of how the versions are related. The versions are given in different notations connected through a core notation by compilers from and to the notations of existing tools and specification methods. The reasons that translations cannot always be exact are analyzed, based on experience with over ten separate compiler translations among formal methods notations. The ideas of faithful translations and structural similarity are shown and used as a measure of the quality of translations. |