Formally Characterizing the Effect of Model Transformations on System Properties
Presenter: Rikayan Chaki
Session Chair: Marie Farrell
In Model-Driven Software Development, models and model transformations are the primary artefacts to develop software in a structured way. Models have been subjected to formal verification for a long time, but the field of formal model transformation verification is relatively young. Existing techniques, when they focus on the effect transformations have on the system components they are applied on, limit their analysis to checking for the preservation of semantics or particular properties, but it is not always the intention of a transformation to preserve these. We propose an approach to characterize the effect of applying a (formal description of a) model transformation when applied on a component that satisfies a given functional property. The given functional property is formalized in Action-based LTL, and our characterization is captured by a system of modal mu-calculus equations.