|M.Sc Student||Berg Mirit|
|Subject||Property Transformations for Translations|
|Department||Department of Computer Science||Supervisor||Professor Shmuel Katz|
When translating a system description from one specification language to another, it is in many cases inevitable that the underlying models of the original and the translated specification will be different. The notion of property transformation can be used to define the relation between the properties of the original and the translated model. Definitions of 'faithful' transformations are given, along with motivation and examples. Generally, a faithful transformation is a relation between properties of the source specification and the corresponding properties which are true for the target specification.
Generic translations are considered, derived directly from compilers that translate among formal methods model description languages. Property transformations for these translations are proven faithful for CTL*. The notion of an 'effective' source language is defined as the group of source properties which are transformed to properties expressible in the tool associated with the target of the translation. This notion is then used to show that the most general transformation is not always the best.
Necessary conditions for proving the non-existence of property transformations are given, as well as definitions of the strongest possible transformations. Property transformations are required to be independent of the source model, and this is shown to be a necessary restriction so that the transformation reflects the quality of the model translation. The case of translating between different fairness notions is analyzed separately, and it is shown why in this case it is logical to allow the transformation to be somewhat dependent on the source model.
Compositions of model translation stages and, respectively, property transformations are considered. We prove that a composed property transformation is appropriate for sequentially composed model translations that each have faithful property transformations. Even when the translation of the model mixes translations of two previously analyzed stages non-sequentially, we define conditions when the simple composition of the property transformations is still faithful for the result, and prove the conditions for an example.
Finally, a general method for translation validation is shown, in order to complete the transformation correctness proofs by proving that instances of the translations indeed satisfy the assumptions.