Model Search: Formalizing and Automating Constraint Solving in MDE Platforms

  • Mathias Kleiner
  • Marcos Didonet Del Fabro
  • Patrick Albert
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6138)


Model Driven Engineering (MDE) and constraint programming (CP) have been widely used and combined in different applications. However, existing results are either ad-hoc, not fully integrated or manually executed. In this article, we present a formalization and an approach for automating constraint-based solving in a MDE platform. Our approach generalizes existing work by combining known MDE concepts with CP techniques into a single operation called model search. We present the theoretical basis for model search, as well as an automated process that details the involved operations. We validate our approach by comparing two implemented solutions (one based on Alloy/SAT, the other on OPL/CP), and by executing them over an academic use-case.


Search Engine Model Transformation Constraint Programming Software Product Line Model Search 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Cook, S.A.: The complexity of theorem-proving procedures. In: STOC, pp. 151–158. ACM, New York (1971)Google Scholar
  2. 2.
    Felfernig, A., Friedrich, G., Jannach, D., Zanker, M.: Configuration knowledge representation using uml/ocl. In: Jézéquel, J.-M., Hussmann, H., Cook, S. (eds.) UML 2002. LNCS, vol. 2460, pp. 49–62. Springer, Heidelberg (2002)Google Scholar
  3. 3.
    Petter, A., Behring, A., Muhlhauser, M.: Solving constraints in model transformations. In: Paige, R.F. (ed.) ICMT 2009. LNCS, vol. 5563, pp. 132–147. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  4. 4.
  5. 5.
    Jackson, D.: Automating first-order relational logic. In: FSE, pp. 130–139 (2000)Google Scholar
  6. 6.
    Jouault, F., Bézivin, J.: Km3: A dsl for metamodel specification. In: Gorrieri, R., Wehrheim, H. (eds.) FMOODS 2006. LNCS, vol. 4037, pp. 171–185. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  7. 7.
    Jouault, F., Bézivin, J., Kurtev, I.: TCS: a DSL for the specification of textual concrete syntaxes in model engineering. In: GPCE, pp. 249–254. ACM, New York (2006)CrossRefGoogle Scholar
  8. 8.
    IBM ILOG CPLEX Development Bundle (December 2009),
  9. 9.
  10. 10.
    Cabot, J., Clarisó, R., Riera, D.: Umltocsp: a tool for the formal verification of uml/ocl models using constraint programming. In: ASE, pp. 547–548 (2007)Google Scholar
  11. 11.
    Jouault, J., Kurtev, I.: Transforming Models with ATL. In: Bruel, J.-M. (ed.) MoDELS 2005. LNCS, vol. 3844, pp. 128–138. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  12. 12.
    White, J., Schmidt, D.C., Benavides, D., Trinidad, P., Ruiz-Cortez, A.: Automated diagnosis of product-line configuration errors in feature models. In: Software Product Lines Conference (SPLC 2008), Limmerick, Ireland (2008)Google Scholar
  13. 13.
    Spivey, J.M.: The Z Notation: a reference manual (2001)Google Scholar
  14. 14.
    Kurtev, I., Bezivin, J., Aksit, M.: Technological spaces: An initial appraisal. In: International Symposium on Distributed Objects and Applications (2002)Google Scholar
  15. 15.
    Gogolla, M., Büttner, F., Richters, M.: Use: A uml-based specification environment for validating uml and ocl. Sci. Comput. Program. 69(1-3), 27–34 (2007)zbMATHCrossRefGoogle Scholar
  16. 16.
    Kessentini, M., Sahraoui, H.A., Boukadoum, M.: Model transformation as an optimization problem. In: Czarnecki, K., Ober, I., Bruel, J.-M., Uhl, A., Völter, M. (eds.) MODELS 2008. LNCS, vol. 5301, pp. 159–173. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  17. 17.
    Kleiner, M., Albert, P., Bezivin, J.: Parsing sbvr-based controlled languages. In: Schürr, A., Selic, B. (eds.) MODELS 2009. LNCS, vol. 5795, pp. 122–136. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  18. 18.
  19. 19.
    Nethercote, N., Stuckey, P.J., Becket, R., Brand, S., Duck, G.J., Tack, G.: Minizinc: Towards a standard cp modelling language. In: Bessière, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 529–543. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  20. 20.
    Object Management Group. Meta Object Facility (MOF) 2.0 Query/View/Transformation (QVT) Specification, version 1.0 (2008)Google Scholar
  21. 21.
    OCL 2.0 specification (2008),
  22. 22.
    Clements, P., Northrop, L.: Software Product Lines: Practices and Patterns, 1st edn. Addison-Wesley, Reading (2001)Google Scholar
  23. 23.
    Tessier, P., Servat, D., Gerard, S.: Variability management on behavioral models. In: VaMoS Workshop, pp. 121–130 (2008)Google Scholar
  24. 24.
    Trinidad, P., Benavides, D., Cortés, A.R., Segura, S., Jimenez, A.: Fama framework. In: SPLC, p. 359. IEEE Computer Society, Los Alamitos (2008)Google Scholar
  25. 25.
    Chenouard, R., Granvilliers, L., Soto, R.: Model-driven constraint programming. In: 10th ACM SIGPLAN PPDP, Valence, Spain (2008)Google Scholar
  26. 26.
    SAT4J. A SATisfiability libray for Java (2010),
  27. 27.
    Junker, U., Mailharro, D.: The logic of (j)configurator: Combining constraint programming with a description logic. In: IJCAI 2003. Springer, Heidelberg (2003)Google Scholar
  28. 28.
    Hentenryck, P.V.: The Optimization Programming Language. MIT Press, Cambridge (1999)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Mathias Kleiner
    • 1
  • Marcos Didonet Del Fabro
    • 2
  • Patrick Albert
    • 2
  1. 1.Arts et Metiers ParisTech, CNRS, LSIS LaboratoryFrance
  2. 2.IBM Software GroupFrance

Personalised recommendations