Formal analysis of model transformations

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

In model-driven desing an analysis model is derived from an engeenering model by a model transformation. The errors of the model transformations can invalidate the advantages of precision of the mathematical model. So adviseable to garantee the fail-safeness of model transformations by formal verification.

The paradigm of graph transformations offers an intuitive, well designable and as well precise formal method to specify model transformations. Graph transformation systems potentially induce an infinite state space, which significantly hinders formal verification to guarantee their correctness. Shape analysis is one of the techniques which addresses the formal verification of such infinite state systems. In shape analysis the graphs of the state space are categorised into finite number of groups. Applying the abstract equivalent of graph transformation rules on the shapes an abstract state space is got, which on which one can prove the correctness of graph languages.

There are two main trend in the literature for shape analysis. The first, so called neighbourhood shapes categorises the graphs by the context of their nodes, the second represents the states graph by 3-valued logic structures. These methods can solve problems with different characterisation with variant efficiency.

In the current thesis, I propose to unify the definition of these techniques based on the equivalence of of the graph elements, where both abstractions can be represented by a proper parameterisation. With the unified description, in the view of the problem and by the combination of the parameters the the probability of succesful and realizable analysis can be increased.

In the this thesis I made a feasibility study of the realisation of the common method on VIATRA2 model transformation system, because it able to manage big model spaces and with the use of incremental pattern matching the operations are executed effectively.

Downloads

Please sign in to download the files of this thesis.