Combining termination proofs in model transformation systems. (26th June 2014)

• Record Type: Journal Article
• Authors: BISZTRAY, DÉNES; HECKEL, REIKO
• Is Part Of: Mathematical structures in computer science. Volume 24:Number 4(2014)
• Publication Date: 2014-06-26
• Subjects: Computer science -- Mathematics -- Periodicals; 004.015105
• DOI: 10.1017/S0960129512000369
• Languages: English
• ISSNs: 0960-1295

Abstract

Abstract : In model transformations, where source models are automatically translated into target models or code, termination is necessary for the transformation to be well defined. There are a number of specific termination criteria that can be used when specifying model transformations by graph transformation, though termination is undecidable in general. Unfortunately, and particularly for large and heterogeneous specifications, it is often not possible to use a single termination criterion. In this paper, we propose an approach that applies different criteria to suitable subsets of rules so that termination can be shown locally using the most suitable technique for each subset. Global termination then follows if certain causal dependencies between rules in different subsets are acyclic. The theory is developed at the level of typed attributed graphs, and is motivated and illustrated by a case study translating UML activity diagrams to CSP.