Using mucalculus to define the semantics of the QVTR language

16:30 14th May 2013 ( week 4, Trinity Term 2013 )Lecture Theatre B
In software engineering, bidirectional model transformations are a tool for maintaining (or just checking) consistency between different models of systems  for example, the models corresponding to different subprojects' views of the whole system. QVTR is an industry standard language from the Object Management Group for describing such transformations. Stevens earlier gave a gamebased semantics for checkonly QVTR transformations. She restricted socalled "when" and "where" clauses, parts of the relation definition, to be conjunctions of relation invocations only, and like the OMG standard, did not consider cases in which a relation might (directly or indirectly) invoke itself recursively.
In FASE 2012, we showed how to interpret checkonly QVTR  or any future model transformation language structured similarly  in the mucalculus and use its wellunderstood modelchecking game to lift these restrictions. The interpretation via fixpoints gives a principled argument for assigning semantics to recursive transformations. We demonstrate that a particular class of recursive transformations must be ruled out due to monotonicity considerations. We demonstrate and justify a corresponding extension to the rules of the QVTR game.
In FASE 2013, we extended this further for the "enforce" mode, in which the target model is changed to match the source mode. This work exposed some flaws in the (informal) standard, and pointed up some inherent problems that must be addressed by any implementation. This talk gives an overview of this recent work. The talk will remain at a fairly abstract level, and will not assume prior knowledge of QVTR or mucalculus.
This is joint work with Perdita Stevens.