Using mu-calculus to define the semantics of the QVT-R language
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 sub-projects' views of the whole system. QVT-R is an industry standard language from the Object Management Group for describing such transformations. Stevens earlier gave a game-based semantics for checkonly QVT-R transformations. She restricted so-called "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 QVT-R -- or any future model transformation language structured similarly -- in the mu-calculus and use its well-understood model-checking 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 QVT-R 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 QVT-R or mu-calculus.
This is joint work with Perdita Stevens.