Concretisation of abstract models using constraint solving problems

OData support
Supervisor:
Szatmári Zoltán
Department of Measurement and Information Systems

Nowadays the testing of autonomous agents is a growing problem. In the past to perform the testing of a new agent, real-life environments had to be built where the tests could be carried out. Usually this consumed a lot of time and money. In contrast, the testing of these agents in a virtual environment would be much faster and less expensive. The biggest disadvantage of the generation of the virtual environments is that the domain of the attributes in the environmental models must not be too large, because that can lead to state space explosion. Because of that in the first iteration only the generation of an abstract model is possible, however for further use we need concrete data.

My task is to create a solution to generate the models containing concrete data from the models only containing abstract attributes and relations. The main part of the concretization of abstract models consists of the solving of a constraint satisfaction problem (CSP) generated from the abstract data. The rest of the program is providing the CSP in proper format, processing the solution and updating the original model with the concretized data.

The full process consists of several distinct units, each one of them built around an already existing technology. The traversal and the management of the models are done by the usage of the Eclipse Modeling Framework (EMF). The file containing the constraint satisfaction problem is generated by the Acceleo Eclipse plugin, which can be used for model-to-code (M2C) translation based on a provided template. In the next step the CSP is solved by the Microsoft Z3 SMT solver resulting in a text file containing the concretized data. The interpretation of this text is done by another Eclipse plugin called xText. This tool can be used to process a text based on a domain specific language defined by an xText grammar. The last step in the process is to update the original model with the concrete data by traversing it again via the Eclipse Modeling Framework.

This thesis presents the technologies and tools used to construct the program, and describes the process of the concretization of abstract environmental models in details.

Downloads

Please sign in to download the files of this thesis.