Formal verification of model transformations by shape analysis

OData support
Dr. Varró Dániel
Department of Measurement and Information Systems

Complex design environments based on Domain-Specific Languages (DSLs) are widely used in various phases of model driven development from specification to testing in order to capture the main concepts and relations in the application domain. A precise system model captured in a DSL enables formal analysis and automated code or test generation of proven quality. Unfortunately, the specification of DSL may itself contain conceptual flaws, which invalidates the results of subsequent formal analysis of the system model. The main objective of the current thesis is to provide formal analysis of a DSL itself to highlight inconsistency, incompleteness or ambiguity in DSL specifications.

However, the consistency analysis of DSLs is a difficult task due to (i) decidability problems of handling complex DSLs, (ii) theoretical challenges of supporting well-formedness constraints and derived features, and (iii) the engineering problem of providing a DSL validation tool that is operable by the DSL developer without any extra validation skills.

In this report, I address these challenges by providing (i) a mapping of well-formedness rules and derived features formulated in different constraint languages into first-order logic theories processed by SMT-solvers, (ii) powerful approximations to map complex structures into an efficiently analyzable fragment of first order logic, and (iii) a DSL validation tool seamlessly integrated into industrial modeling frameworks (EMF) where inconsistencies retrieved by SMT-solvers are available as regular DSL instance models.

The DSL validation framework is based on a mapping, which takes an EMF metamodel with derived features, a set of well-formedness constraints (captured in OCL or graph patterns of EMF-IncQuery) and a partial model as input. This partial model is completed by introducing new model elements to it which are compliant with the DSL specification using the generated axioms and underlying theories of the Z3 SMT-solver in the background.

I report on successful use of our validation framework in two complex case studies with industrial requirements. In a collaborative project with a Brazilian airframer, the consistency of EMF metamodels augmented with well-formedness constraints and derived features defined by IncQuery graph patterns is checked to detect design flaws in the early phase of the DSL development. The case study of the R3COP ARTEMIS project that aims to develop safety critical autonomous systems like industrial robots. Our validation framework supported the automatic generation of concrete test cases.


Please sign in to download the files of this thesis.