Improved OCL Expression Evaluation on Henshin Generated State Spaces

Improved OCL Expression Evaluation on Henshin Generated State Space

Model checking faces rising relevancy in many scientific and industrial areas. This can also be observed within the field of Model Engineering where OCL expressions support formulation of versatile constraints for models and furthermore also for state spaces emerging from incremental appliance of model transformations on models. But checking OCL expressions over state spaces means verification of all constraints in every single intermediate state. This clearly leads to tremendous efficiency and performance issues when accomplished with primitive approaches. Within this article we will demonstrate possible improvements to overcome these issues.

Background

Generally very different ambitions exist for using OCL expressions that need efficient analysis. Basically at least two different research directions can be identified. The first one deals with OCL expression evaluation within IDEs to support developers working on huge heterogeneous models with often many and complex OCL expressions. Here efficiency is important because humans working with IDEs usually expect fast responses on their actions. It is in no way satisfying for modellers when changes on their models or OCL expressions trigger evaluation cycles taking minutes to present results. Normally this should be accomplished in background and real-time to provide immediate feedback on the impacts of modellers actions.

The second one deals with evaluation of less complex OCL expressions on big homogeneous data like for example databases or state spaces representing possible program execution paths. The importance of efficiency arises here from the size of the model and not from the real-time feedback to the user. Otherwise consistency evaluation of growing models gets fast intractable and another approach must be taken.

Implementation

There exist for both theoretical directions practical solutions but implementations can vary strongly. For implementing real-time evaluation of complex models with complex constraints, approaches like graph pattern matching proved usable. In this case constraints are defined as rules in form of graph patterns which are matched against the underlying models that have to be evaluated and also exist in form of graphs. Another possibility is to keep meta-data about the model structure and state, optimize OCL expressions before usage by splitting them up or simplifying them and use meta-data in addition to the model applied change events, to get a high-performance solution. Another approach for evaluation of constraints on big datasets works with a conversion from OCL to the Monoid Calculus. The models to be evaluated are stored within databases and the transformed constraints are furthermore expressed as related stored procedures. This supports efficient execution within database environments.

Generally important for nearly all approaches is to consider, that not the whole model should be evaluated every time a change is applied to it but to start with a clean state and iteratively retrieve all change events on the model to estimate, whether specific constraints could be effected or not. This assures that the model is always kept in a valid state and that efficiency is not affected by growing data amounts.

Laboratory Environment and Approach

We will give insights into the environment and our approach for the laboratory part of our work. As environment the Eclipse Modelling Framework was chosen together with the integrated Eclipse OCL implementation. Eclipse OCL provides a feature promising iterative and efficient evaluation of OCL constraints on EMF models called Impact Analyzer. We decided to chose an approach based on it with Henshin for state space generation. The combination of these formed the base of our laboratory work. Setting up the environment is mostly straight forward but one important special adaptation is necessary to reproduce the exact environment we used. Some dependencies must be manually added to the project because they aren't available out of the box. The following figure provides detailed information about which ones must be added.

Gossiping Girls Problem

We chose the Gossiping Girls Problem as a starting point of our research. It is based on a group of girls, in which each can have an arbitrary number of secrets. A girl can start a phone call with any other girl of the group. The girl knows after this phone call all unknown secrets of the other girl and vice versa. The question to answer is how many calls are at most necessary until each girl knows all existing secrets of the others. The related EMF Ecore model for the problem is provided in the following graph.

To generate a state space with Henshin, suitable transformation rules which represent the necessary behaviour for the problem must be provided. We present them in the following graph.

 

Impact Analyzer on Henshin State Space

For integration of the functionality from the Impact Analyzer into Henshin generated state spaces and the immanent OCL expression evaluation, the overall Henshin internal processing must be adapted and changed. The first problem is that Henshin, at the beginning generates by iterative applying rules the complete state space and afterwards evaluates OCL constraints on it as a whole. This technique is especially bad for state spaces growing much bigger than available memory can hold. For this reason we changed the behaviour to an iterative one. So the state space is expanded by applying transformation rules once and afterwards triggering OCL expression evaluation on the expanded set. The previous set can be reduced to free space for new expansions. Furthermore this stepwise approach also supports integration of the Impact Analyzer which works in an event listening and model intrusive way.

Results and Benchmarks

Unfortunately the desired positive effects and efficiency improvements promised by the Impact Analyzer could not be achieved during our test setup. This is due, however, to the way Henshin stores the models resulting from a single step exploration of the state space. We suppose that Henshin generates a new set of models during the state space generation procedure, thus invalidating the change event listeners the Impact Analyzer depends on to compute necessary re-evaluations for a given OCL expression. Therefore the following benchmarks will not provide any performance improvements but due to the changed stepwise processing of OCL expression evaluation the time consumption of executions rose dramatically.

Without Impact Analayzer

With Impact Analayzer

Further Work

The next steps of research to reach the desired goal in this context would deal with the following issues:

1. Detailed analysis of the underlying EMF model data structure managed by Henshin in relation to the EMF model of the Gossiping Girls Problem.
2. Code analysis of the stepwise exploration processing to understand how Henshin decides, which transitions will be added to the model of the previous step.
3. Investigate how Henshin maintains the data structure between different exploration steps.
4. Try to find a solution for a working integration of the Impact Analyzer with the gained knowledge of the previous steps.