Movatterモバイル変換

[0]ホーム
URL:

Skip to main content

Advertisement

Springer Nature Link
Log in

Target Oriented Relational Model Finding

  • Conference paper

Part of the book series:Lecture Notes in Computer Science ((LNTCS,volume 8411))

  • 1333Accesses

Abstract

Model finders are becoming useful in many software engineering problems. Kodkod [19] is one of the most popular, due to its support for relational logic (a combination of first order logic with relational algebra operators and transitive closure), allowing a simpler specification of constraints, and support for partial instances, allowing the specification ofa priori (exact, but potentially partial) knowledge about a problem’s solution. However, in some software engineering problems, such as model repair or bidirectional model transformation, knowledge about the solution is not exact, but instead there is a known target that the solution should approximate. In this paper we extend Kodkod’s partial instances to allow the specification of such targets, and show how its model finding procedure can be adapted to support them (using both PMax-SAT solvers or SAT solvers with cardinality constraints). Two case studies are also presented, including a careful performance evaluation to assess the effectiveness of the proposed extension.

Similar content being viewed by others

Keywords

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.

References

  1. Asín, R., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: Cardinality networks: a theoretical and empirical study. Constraints 16(2), 195–221 (2011)

    Article MATH MathSciNet  Google Scholar 

  2. Cha, B., Iwama, K., Kambayashi, Y., Miyazaki, S.: Local search algorithms for partial MAXSAT. In: AAAI 1997, pp. 263–268. AAAI (1997)

    Google Scholar 

  3. Czarnecki, K., Foster, J., Hu, Z., Lämmel, R., Schürr, A., Terwilliger, J.: Bidirectional transformations: A cross-discipline perspective. In: Paige, R.F. (ed.) ICMT 2009. LNCS, vol. 5563, pp. 260–283. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  4. Edwards, J., Jackson, D., Torlak, E.: A type system for object models. In: FSE 2004, pp. 189–199. ACM (2004)

    Google Scholar 

  5. Fu, Z., Malik, S.: On solving the partial MAX-SAT problem. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 252–265. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  6. Jackson, D.: Software Abstractions: Logic, Language, and Analysis, revised edn. MIT Press (2012)

    Google Scholar 

  7. Macedo, N., Cunha, A.: Implementing QVT-R bidirectional model transformations using Alloy. In: Cortellessa, V., Varró, D. (eds.) FASE 2013. LNCS, vol. 7793, pp. 297–311. Springer, Heidelberg (2013)

    Google Scholar 

  8. Macedo, N., Guimarães, T., Cunha, A.: Model repair and transformation with Echo. In: ASE 2013, pp. 694–697. IEEE (2013)

    Google Scholar 

  9. Maglalang, J.C.: Native cardinality constraints: More expressive, more efficient constraints. Honors Projects, Paper 19. Illinois Wesleyan University (2012)

    Google Scholar 

  10. Milicevic, A., Jackson, D.: Preventing arithmetic overflows in Alloy. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 108–121. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  11. Miyazaki, S., Iwama, K., Kambayashi, Y.: Database queries as combinatorial optimization problems. In: CODAS 1996, pp. 448–454 (1996)

    Google Scholar 

  12. Nelson, T., Saghafi, S., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: Aluminum: principled scenario exploration through minimality. In: ICSE 2013, pp. 232–241. IEEE (2013)

    Google Scholar 

  13. OMG: MOF 2.0 Query/View/Transformation specification (QVT), version 1.1 (January 2011),http://www.omg.org/spec/QVT/1.1/

  14. Reder, A., Egyed, A.: Computing repair trees for resolving inconsistencies in design models. In: ASE 2012, pp. 220–229. ACM (2012)

    Google Scholar 

  15. Reiter, R.: A theory of diagnosis from first principles. Artificial Intelligence 32(1), 57–95 (1987)

    Article MATH MathSciNet  Google Scholar 

  16. Van Der Straeten, R., Pinna Puissant, J., Mens, T.: Assessing the Kodkod Model Finder for Resolving Model Inconsistencies. In: France, R.B., Kuester, J.M., Bordbar, B., Paige, R.F. (eds.) ECMFA 2011. LNCS, vol. 6698, pp. 69–84. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  17. Tarjan, R.: Depth-first search and linear graph algorithms. SIAM Journal on Computing 1(2), 146–160 (1972)

    Article MATH MathSciNet  Google Scholar 

  18. Torlak, E., Jackson, D.: The design of a relational engine. Tech. Rep. MIT-CSAIL-TR-2006-068, MIT (2006)

    Google Scholar 

  19. Torlak, E., Jackson, D.: Kodkod: A relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632–647. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  20. Xiong, Y., Hubaux, A., She, S., Czarnecki, K.: Generating range fixes for software configuration. In: ICSE 2012, pp. 58–68. IEEE (2012)

    Google Scholar 

  21. Nokhbeh Zaeem, R., Khurshid, S.: Contract-based data structure repair using Alloy. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 577–598. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. HASLab — High Assurance Software Laboratory, INESC TEC, Universidade do Minho, Braga, Portugal

    Alcino Cunha, Nuno Macedo & Tiago Guimarães

Authors
  1. Alcino Cunha

    You can also search for this author inPubMed Google Scholar

  2. Nuno Macedo

    You can also search for this author inPubMed Google Scholar

  3. Tiago Guimarães

    You can also search for this author inPubMed Google Scholar

Editor information

Editors and Affiliations

  1. CNR, Pisa, Italy

    Stefania Gnesi

  2. University of Twente, Enschede, The Netherlands

    Arend Rensink

Rights and permissions

Copyright information

© 2014 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Cunha, A., Macedo, N., Guimarães, T. (2014). Target Oriented Relational Model Finding. In: Gnesi, S., Rensink, A. (eds) Fundamental Approaches to Software Engineering. FASE 2014. Lecture Notes in Computer Science, vol 8411. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54804-8_2

Download citation

Publish with us

[8]ページ先頭
©2009-2025 Movatter.jp