Foundational Analysis Techniques for High-Level Transformation Programs
Research output: Book / Anthology / Report / Ph.D. thesis › Ph.D. thesis
The goal of this dissertation is to develop foundational techniques and prototype tools for verifying transformation programs, based on techniques from traditional programming language research. At first, I present a systematic analysis of declarative highlevel transformation languages, like QVT and ATL, seeking to clarify their expressiveness. The analysis showed that virtually all examined languages were Turing-complete and thus could not be treated specially for verification.
I describe a joint effort in designing and validating an industrial modernization project using the high-level transformation language TXL. The transformation was validated using the translation validation and symbolic execution, catching 50 serious bug cases in an otherwise well-tested expert-written transformation, and thus showing the need for verification tools in this domain.
Using these experiences, I develop a formal symbolic execution algorithm for a small transformation language capturing key high-level constructs. A proto-type white-box test generation tool was implemented using the algorithm, and evaluated on a series of refactorings and model transformations comparing favorably against baseline black-box test generator in terms of test coverage.
I present the first formal operational semantics for a large subset of Rascal, called Rascal Light, which has been validated by formally proving a series of semantic properties regarding strong typing, safety and termination. This creates a solid basis for further foundational work on high-level transformation languages.
Finally, I develop a formal abstract interpreter for Rascal Light,
with a modular abstract domain design and a Schmidt-style abstract operational semantics, adapting the idea of widening by trace memoization to work with inputs from infinite domains. The technique is evaluated on real Rascal transformations, showing that it is possible to effectively verify target type and shape properties.
|Publisher||IT-Universitetet i København|
|Number of pages||316|
|Publication status||Published - 2018|