SpringerLink
Log in

Extensive Validation of OCL Models by Integrating SAT Solving into USE

  • Conference paper
Objects, Models, Components, Patterns (TOOLS 2011)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 6705))

Abstract

The Object Constraint Language (OCL) substantially enriches modeling languages like UML, MOF or EMF with respect to formulating meaningful model properties. In model-centric approaches, an accurately defined model is a requisite for further use. During development of a model, continuous validation of properties and feedback to developers is required, since many design flaws can then be directly discovered and corrected. For this purpose, lightweight validation approaches which allow developers to perform automatic model analysis are particularly helpful. We provide a new method for efficiently searching for model instances. The existence or non-existence of model instances with certain properties allows significant conclusions about model properties. Our approach is based on the translation of UML and OCL concepts into relational logic and its realization with SAT solvers. We explain various use cases of our proposal, for example, completion of partly defined model instances so that particular properties hold in the completed model instances. Our proposal is realized by integrating a model validator as a plugin into the UML and OCL tool USE.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: On challenges of model transformation from UML to Alloy. SoSyM 9(1), 69–86 (2010)

    Google Scholar 

  2. Berardi, D., Calvanese, D., Giacomo, G.D.: Reasoning on UML class diagrams. Artif. Intell. 168(1-2), 70–118 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  3. Blanchette, J.C., Nipkow, T.: Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131–146. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  4. Brucker, A.D., Wolff, B.: HOL-OCL: A Formal Proof Environment for UML/OCL. In: FASE, pp. 97–100 (2008)

    Google Scholar 

  5. Cabot, J., Clarisó, R., Riera, D.: Verification of UML/OCL Class Diagrams using Constraint Programming. In: Proc. 2008 IEEE Int. Conf. Software Testing Verification and Validation Workshop, pp. 73–80. IEEE Computer Society Press, Washington, DC, USA (2008)

    Chapter  Google Scholar 

  6. Chiorean, D., Pasca, M., Cârcu, A., Botiza, C., Moldovan, S.: Ensuring UML Models Consistency Using the OCL Environment. Electr. Notes Theor. Comput. Sci. 102, 99–110 (2004)

    Article  Google Scholar 

  7. Clavel, M., Egea, M.: ITP/OCL: A Rewriting-Based Validation Tool for UML+OCL Static Class Diagrams. In: AMAST, pp. 368–373 (2006)

    Google Scholar 

  8. Demuth, B., Wilke, C.: Model and Object Verification by Using Dresden OCL. In: Proc. Russian-German Workshop Innovation Information Technologies: Theory and Practice, p. 81. Technical University, Ufa (2009)

    Google Scholar 

  9. Gogolla, M., Bohling, J., Richters, M.: Validating UML and OCL Models in USE by Automatic Snapshot Generation. SoSyM 4(4), 386–398 (2005)

    Google Scholar 

  10. Gogolla, M., Büttner, F., Richters, M.: USE: A UML-Based Specification Environment for Validating UML and OCL. SCP 69, 27–34 (2007)

    MathSciNet  MATH  Google Scholar 

  11. Gogolla, M., Kuhlmann, M., Hamann, L.: Consistency, independence and consequences in UML and OCL models. In: Dubois, C. (ed.) TAP 2009. LNCS, vol. 5668, pp. 90–104. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  12. Gogolla, M., Vallecillo, A.: Tractable Model Transformation Testing. In: France, R., Küster, J.M., Bordbar, B., Paige, R.F. (eds.) Proc. 7th Int. Conf. Modelling Foundations and Applications (ECMFA 2011). LNCS, Springer, Berlin (2011)

    Google Scholar 

  13. Jackson, D.: Software Abstractions - Logic, Language, and Analysis. The MIT Press, Cambridge (2006)

    Google Scholar 

  14. Jeanneret, C., Eyer, L., Markovic, S., Baar, T.: RoclET- Refactoring OCL Expressions by Transformations. In: Software & Systems Engineering and their Applications,19th International Conference, ICSSEA 2006 (2006)

    Google Scholar 

  15. Kelsen, P., Ma, Q.: A lightweight approach for defining the formal semantics of a modeling language. In: Busch, C., Ober, I., Bruel, J.-M., Uhl, A., Völter, M. (eds.) MODELS 2008. LNCS, vol. 5301, pp. 690–704. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  16. Kolovos, D., Rose, L., Paige, R.: The epsilon Book , http://www.eclipse.org/gmt/epsilon/doc/book/

  17. Kuhlmann, M., Sohr, K., Gogolla, M.: Comprehensive Two-level Analysis of Static and Dynamic RBAC Constraints with UML and OCL. In: Baik, J., Massacci, F., Zulkernine, M. (eds.) Fifth International Conference on Secure Software Integration and Reliability Improvement, SSIRI 2011, IEEE Computer Society, Los Alamitos (2011)

    Google Scholar 

  18. de Lara, J., Guerra, E.: Deep meta-modelling with metaDepth. In: Vitek, J. (ed.) TOOLS 2010. LNCS, vol. 6141, pp. 1–20. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  19. Ornaghi, M., Fiorentini, C., Momigliano, A., Pagano, F.: Applying ASP to UML model validation. In: Erdem, E., Lin, F., Schaub, T. (eds.) LPNMR 2009. LNCS, vol. 5753, pp. 457–463. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  20. Queralt, A., Teniente, E.: Reasoning on UML class diagrams with OCL constraints. In: Embley, D.W., Olivé, A., Ram, S. (eds.) ER 2006. LNCS, vol. 4215, pp. 497–512. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  21. Samimi, H., Aung, E.D., Millstein, T.: Falling back on executable specifications. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 552–576. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  22. Soeken, M., Wille, R., Kuhlmann, M., Gogolla, M., Drechsler, R.: Verifying UML/OCL Models Using Boolean Satisfiability. In: Müller, W. (ed.) Proc. Design, Automation and Test in Europe (DATE 2010 ). IEEE Computer Society Press, Los Alamitos (2010)

    Google Scholar 

  23. 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 

  24. Torlak, E., Vaziri, M., Dolby, J.: MemSAT: checking axiomatic specifications of memory models. SIGPLAN Not. 45, 341–350 (2010), http://doi.acm.org/10.1145/1809028.1806635

    Article  Google Scholar 

  25. Treharne, H., Schneider, S., Grant, N., Evans, N., Ifill, W.: A step towards merging xUML and CSP \({\| \ }\)B. In: Abrial, J.-R., Glässer, U. (eds.) Rigorous Methods for Software Construction and Analysis. LNCS, vol. 5115, pp. 130–146. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  26. Trong, T.D., Ghosh, S., France, R.B., Hamilton, M., Wilkins, B.: UMLAnT: An Eclipse Plugin for Animating and Testing UML Designs. In: Proc. OOPSLA workshop Eclipse technology eXchange, pp. 120–124. ACM Press, New York (2005)

    Google Scholar 

  27. Wegmann, A., Le, L.S., Hussami, L., Beyer, D.: A Tool for Verified Design using Alloy for Specification and CrocoPat for Verification. In: Jackson, D., Zave, P. (eds.) Proc. First Alloy Workshop (2006)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, Database Systems Group, University of Bremen, D-28334, Bremen, Germany

    Mirco Kuhlmann, Lars Hamann & Martin Gogolla

Authors
  1. Mirco Kuhlmann
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Lars Hamann
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Martin Gogolla
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Microsoft Research, One Microsoft Way, 98052-6399, Redmond, WA, USA

    Judith Bishop

  2. ETSI Informática Bulevar, University of Málaga, Louis Pasteur 35, 29071, Málaga, Spain

    Antonio Vallecillo

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kuhlmann, M., Hamann, L., Gogolla, M. (2011). Extensive Validation of OCL Models by Integrating SAT Solving into USE. In: Bishop, J., Vallecillo, A. (eds) Objects, Models, Components, Patterns. TOOLS 2011. Lecture Notes in Computer Science, vol 6705. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21952-8_21

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-21952-8_21

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-21951-1

  • Online ISBN: 978-3-642-21952-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation