Skip to main content
SpringerLink
Log in

From UML and OCL to Relational Logic and Back

  • Conference paper
Model Driven Engineering Languages and Systems (MODELS 2012)

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

Abstract

Languages like UML and OCL are used to precisely model systems. Complex UML and OCL models therefore represent a crucial part of model-driven development, as they formally specify the main system properties. Consequently, creating complete and correct models is a critical concern. For this purpose, we provide a lightweight model validation method based on efficient SAT solving techniques. In this paper, we present a transformation from UML class diagram and OCL concepts into relational logic. Relational logic in turn represents the source for advanced SAT-based model instance finders like Kodkod. This paper focuses on a natural transformation approach which aims to exploit the features of relational logic as directly as possible through straitening the handling of main UML and OCL features. This approach allows us to explicitly benefit from the efficient handling of relational logic in Kodkod and to interpret found results backwards in terms of UML and OCL.

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

Access this chapter

Log in via an institution
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 shipping 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.

References

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

    Article  Google Scholar 

  2. Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (2009)

    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. Braga, B.F.B., Almeida, J.P.A., Guizzardi, G., Benevides, A.B.: Transforming OntoUML into Alloy: towards conceptual model validation using a lightweight formal method. ISSE 6(1-2), 55–63 (2010)

    Google Scholar 

  5. Brucker, A.D., Wolff, B.: HOL-OCL: A Formal Proof Environment for uml/ocl. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961, pp. 97–100. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  6. Cabot, J., Clariso, R., Riera, D.: Verification of UML/OCL Class Diagrams using Constraint Programming. In: IEEE International Conference on Software Testing Verification and Validation Workshop, ICSTW 2008, pp. 73–80 (April 2008)

    Google Scholar 

  7. Clavel, M., Egea, M.: ITP/OCL: A Rewriting-Based Validation Tool for UML+OCL Static Class Diagrams. In: Johnson, M., Vene, V. (eds.) AMAST 2006. LNCS, vol. 4019, pp. 368–373. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  8. Garis, A.G., Cunha, A., Riesco, D.: Translating Alloy Specifications to UML Class Diagrams Annotated with OCL. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 221–236. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  9. 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)

    Article  MATH  Google Scholar 

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

    Google Scholar 

  11. Krieger, M.P., Brucker, A.D.: Extending OCL Operation Contracts with Objective Functions. ECEASST 44 (2011)

    Google Scholar 

  12. Krieger, M.P., Knapp, A.: Executing Underspecified OCL Operation Contracts with a SAT Solver. ECEASST 15 (2008)

    Google Scholar 

  13. Kuhlmann, M., Gogolla, M.: Intrinsic Relational Approach: Transformation of OCL Operations, http://www.db.informatik.uni-bremen.de/publications/intern/IntrinsicApproachOCL2012.pdf

  14. Kuhlmann, M., Gogolla, M.: Strengthening SAT-Based Validation of UML/OCL Models by Representing Collections as Relations. In: Tolvanen, J.P., Vallecillo, A. (eds.) ECMFA 2012. LNCS, vol. 7349, pp. 32–48. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  15. Kuhlmann, M., Hamann, L., Gogolla, M.: Extensive Validation of OCL Models by Integrating SAT Solving into USE. In: Bishop, J., Vallecillo, A. (eds.) TOOLS 2011. LNCS, vol. 6705, pp. 290–306. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  16. Kuhlmann, M., Hamann, L., Gogolla, M., Büttner, F.: A benchmark for OCL engine accuracy, determinateness, and efficiency. Software and System Modeling 11(2), 165–182 (2012)

    Article  Google Scholar 

  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.) SSIRI 2011, pp. 108–117. IEEE (2011)

    Google Scholar 

  18. Maoz, S., Ringert, J.O., Rumpe, B.: CD2Alloy: Class Diagrams Analysis Using Alloy Revisited. In: Whittle, J., Clark, T., Kühne, T. (eds.) MODELS 2011. LNCS, vol. 6981, pp. 592–607. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  19. Maoz, S., Ringert, J.O., Rumpe, B.: Semantically Configurable Consistency Analysis for Class and Object Diagrams. In: Whittle, J., Clark, T., Kühne, T. (eds.) MODELS 2011. LNCS, vol. 6981, pp. 153–167. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  20. Olivé, A.: Conceptual Modeling of Information Systems. Springer (2007)

    Google Scholar 

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

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

  23. Roldán, M., Durán, F.: Dynamic Validation of OCL Constraints with mOdCL. ECEASST 44 (2011)

    Google Scholar 

  24. Rumbaugh, J., Jacobson, I., Booch, G.: Unified Modeling Language Reference Manual, 2nd edn. The Pearson Higher Education (2004)

    Google Scholar 

  25. Samimi, H., Aung, E.D., Millstein, T.D.: Falling Back on Executable Specifications. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 552–576. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  26. Soeken, M., Wille, R., Kuhlmann, M., Gogolla, M., Drechsler, R.: Verifying UML/OCL models using Boolean satisfiability. In: DATE, pp. 1341–1344. IEEE (2010)

    Google Scholar 

  27. Straeten, R.V.D., Puissant, J.P., Mens, T.: Assessing the Kodkod Model Finder for Resolving Model Inconsistencies. In: France, R.B., Küster, J.M., Bordbar, B., Paige, R.F. (eds.) ECMFA 2011. LNCS, vol. 6698, pp. 69–84. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

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

  29. Torlak, E., Vaziri, M., Dolby, J.: MemSAT: checking axiomatic specifications of memory models. In: Zorn, B.G., Aiken, A. (eds.) PLDI, pp. 341–350. ACM (2010)

    Google Scholar 

  30. Warmer, J., Kleppe, A.: The Object Constraint Language: Getting Your Models Ready for MDA. The Addison-Wesley Object Technology Series. Addison-Wesley (2003)

    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 & Martin Gogolla

Authors
  1. Mirco Kuhlmann
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Martin Gogolla
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Colorado State University, 80523, Fort Collins, CO, USA

    Robert B. France

  2. Healthcare Services International, Managed Services, Siemens AG, Hartmannstr. 16, 91052, Erlangen, Germany

    Jürgen Kazmeier

  3. Institute of Computer Science, University of Innsbruck, Technikerstr. 21a, 6020, Innsbruck, Austria

    Ruth Breu

  4. Software Engineering Group, A5, 6, University of Mannheim, 68131, Mannheim, Germany

    Colin Atkinson

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kuhlmann, M., Gogolla, M. (2012). From UML and OCL to Relational Logic and Back. In: France, R.B., Kazmeier, J., Breu, R., Atkinson, C. (eds) Model Driven Engineering Languages and Systems. MODELS 2012. Lecture Notes in Computer Science, vol 7590. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33666-9_27

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-33666-9_27

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-33665-2

  • Online ISBN: 978-3-642-33666-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation