Skip to Main content Skip to Navigation
Journal articles

Slicing ATL Model Transformations for Scalable Deductive Verification and Fault Localization

Abstract : Model-driven engineering (MDE) is increasingly accepted in industry as an effective approach for managing the full life cycle of software development. In MDE, software models are manipulated, evolved and translated by model transformations (MT), up to code generation. Automatic deductive verification techniques have been proposed to guarantee that transformations satisfy correctness requirements (encoded as transformation contracts). However, to be transferable to industry, these techniques need to be scalable and provide the user with easily accessible feedback.In MT-specific languages like ATL, we are able to infer static trace information (i.e. mappings among types of generated elements and rules that potentially generate these types). In this paper we show that this information can be used to decompose the MT contract and, for each sub-contract, slice the MT to the only rules that may be responsible for fulfilling it. Based on this contribution, we design a fault localization approach for MT, and a technique to significantly enhance scalability when verifying large MTs against a large number of contracts. We implement both these algorithms as extensions of the VeriATL verification system, and we show by experimentation that they increase its industry-readiness.
Complete list of metadatas

Cited literature [44 references]  Display  Hide  Download
Contributor : Zheng Cheng <>
Submitted on : Wednesday, April 11, 2018 - 10:01:07 AM
Last modification on : Wednesday, June 24, 2020 - 4:19:51 PM


Files produced by the author(s)



Zheng Cheng, Massimo Tisi. Slicing ATL Model Transformations for Scalable Deductive Verification and Fault Localization. International Journal on Software Tools for Technology Transfer, Springer Verlag, 2018, 20 (6), pp.645-663. ⟨10.1007/s10009-018-0491-8⟩. ⟨hal-01763410⟩



Record views


Files downloads