Recursion and Iteration Support in USE Validator with AnATLyzer

5 years 7 months ago
Recursion and Iteration Support in USE Validator with AnATLyzer
Model finders enable numerous verification approaches based on searching the existence of models satisfying certain properties of interest. One of such approaches is anATLyzer, a static analysis tool for ATL transformations, which relies on USE Validator to provide fine grained analysis based on finding witness models that satisfy the OCL path conditions associated to particular errors. However it is limited by the fact that USE Validator does not include built-in support for analysing recursive operations and the iterate collection operator. This paper reports our approach to allow USE Validator to analyse OCL path conditions containing recursive operations and iterate, with the aim of widening the amount of actual transformations that can be processed by anATLyzer. We present our approach, based on unfolding recursion into a finite number of steps, and we discuss how to take into account practical aspects such as inheritance and details about the implementation.
Jesús Sánchez Cuadrado
Added 15 Apr 2016
Updated 15 Apr 2016
Type Journal
Year 2015
Authors Jesús Sánchez Cuadrado
Comments (0)