Dynamic Validation of Maude Prototypes of UML Models

  • Francisco Durán
  • Manuel Roldán
  • Antonio Moreno
  • José María Álvarez
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8373)


We propose an approach for the validation of UML models annotated with OCL constraints. Specifically, we provide support for dynamically validating class invariants and operation pre/post conditions during the execution of prototypes automatically obtained from UML diagrams. The supported UML models specify both static and dynamic aspects, specifically, we focus on class and sequence diagrams. The proposal is based on Maude: UML models and OCL expressions are represented as Maude specifications, which allows us to evaluate OCL expressions on UML models by term rewriting. A model transformation allows us to accomplish this transformation automatically, and represents a first step towards the integration of the proposed facilities into development environments. The Maude specifications thus obtained can be seen as high-level executable prototypes of the annotated UML models.


Model Transformation Class Diagram Sequence Diagram Object Constraint Language Context Object 
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.
  2. 2.
    Ameedeen, M.A., Bordbar, B.: A model driven approach to represent sequence diagrams as free choice Petri Nets. In: 12th Intl. IEEE Enterprise Distributed Object Computing Conf., ECOC 2008, pp. 213–221. IEEE (2008)Google Scholar
  3. 3.
    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)CrossRefGoogle Scholar
  4. 4.
    Booch, G., Rumbaugh, J., Jacobson, I.: The Unified Modeling Language User Guide, 2nd edn. Addison-Wesley (2005)Google Scholar
  5. 5.
    Boronat, A., Meseguer, J.: An Algebraic Semantics for MOF. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961, pp. 377–391. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  6. 6.
    Boronat, A., Meseguer, J.: Algebraic semantics of ocl-constrained metamodel specifications. In: Oriol, M., Meyer, B. (eds.) TOOLS EUROPE 2009. LNBIP, vol. 33, pp. 96–115. Springer, Heidelberg (2009)Google Scholar
  7. 7.
    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)CrossRefGoogle Scholar
  8. 8.
    Cabot, J., Clarisó, R., Riera, D.: Verification of uml/ocl class diagrams using constraint programming. In: First Intl. Conf. on Software Testing, Verification, and Validation, ICST 2008, pp. 73–80. IEEE (2008)Google Scholar
  9. 9.
    Cabot, J., Gogolla, M.: Object constraint language (OCL): A definitive guide. In: Bernardo, M., Cortellessa, V., Pierantonio, A. (eds.) SFM 2012. LNCS, vol. 7320, pp. 58–90. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  10. 10.
    Cabot, J., Teniente, E.: Constraint support in MDA tools: A survey. In: Rensink, A., Warmer, J. (eds.) ECMDA-FA 2006. LNCS, vol. 4066, pp. 256–267. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  11. 11.
    Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.F.: Maude: Specification and Programming in Rewriting Logic. Theoretical Computer Science 285(2), 187–243 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)zbMATHGoogle Scholar
  13. 13.
    Clavel, M., Durán, F., Hendrix, J., Lucas, S., Meseguer, J., Ölveczky, P.: The Maude Formal Tool Environment. In: Mossakowski, T., Montanari, U., Haveraaen, M. (eds.) CALCO 2007. LNCS, vol. 4624, pp. 173–178. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  14. 14.
    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)CrossRefGoogle Scholar
  15. 15.
    Czarnecki, K., Helsen, S.: Feature-based survey of model transformation approaches. IBM Syst. J. 45(3), 621–645 (2006)CrossRefGoogle Scholar
  16. 16.
    Durán, F., Gogolla, M., Roldán, M.: Tracing Properties of UML and OCL Models with Maude. In: Durán, F., Rusu, V. (eds.) Proc. of Intl. Workshop on Algebraic Methods in Model-Based Software Engineering, AMMSE 2011, Electronic Proceedings in Theoretical Computer Science (2011)Google Scholar
  17. 17.
    Durán, F., Roldán, M.: Validating OCL constraints on Maude prototypes of UML models (2012),
  18. 18.
    Fernández-Alemán, J.L., Toval-Álvarez, A.: Seamless Formalizing the UML Semantics through Metamodels. In: Siau, K., Halpin, T. (eds.) Unified Modeling Language: Systems Analysis, Design and Development Issues, pp. 224–248. Idea Group Publishing (2001)Google Scholar
  19. 19.
    Gogolla, M., Büttner, F., Richters, M.: USE: A UML-based Specification Environment for Validating UML and OCL. Science of Computer Programming 69(1-3), 27–34 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Hamann, L., Hofrichter, O., Gogolla, M.: On integrating structure and behavior modeling with OCL. In: France, R.B., Kazmeier, J., Breu, R., Atkinson, C. (eds.) MODELS 2012. LNCS, vol. 7590, pp. 235–251. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  21. 21.
    Jouault, F., Allilaire, F., Bézivin, J., Kurtev, I.: ATL: A model transformation tool. Science of Computer Programming 72(1-2), 31–39 (2008)MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    Jouault, F., Kurtev, I.: Transforming models with ATL. In: Bruel, J.-M. (ed.) MoDELS 2005. LNCS, vol. 3844, pp. 128–138. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  23. 23.
    Knapp, A.: Generating Rewrite Theories from UML Collaborations. In: Futatsugi, K., Nakagawa, A., Tamai, T. (eds.) CAFE: An Industrial-Strength Algebraic Formal Method, pp. 97–120. Elsevier (2000)Google Scholar
  24. 24.
    Kuhlmann, M., Gogolla, M.: From UML and OCL to relational logic and back. In: France, R.B., Kazmeier, J., Breu, R., Atkinson, C. (eds.) MODELS 2012. LNCS, vol. 7590, pp. 415–431. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  25. 25.
    Lund, M.S.: Operational Analysis of Sequence Diagram Specifications. PhD thesis (2007)Google Scholar
  26. 26.
    Lund, M.S., Stølen, K.: Deriving tests from UML 2.0 sequence diagrams with neg and assert. In: Intl. Workshop on Automation of Software Test, AST 2006, pp. 22–28. ACM (2006)Google Scholar
  27. 27.
  28. 28.
    Meseguer, J.: Conditional Rewriting Logic as a Unified Model of Concurrency. Theoretical Computer Science 96, 73–155 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  29. 29.
    Meseguer, J.: 20 years of rewriting logic. Technical report, University of Illinois at Urbana-Champaign (2012),
  30. 30.
    Mokhati, F., Badri, M.: Generating Maude Specifications from UML Use Case Diagrams. Journal of Object Technology 8(2), 136–319 (2009)CrossRefGoogle Scholar
  31. 31.
    Object Management Group. OMG unified modeling language (OMG UML), superstructure, v2.1.2 (formal/2007-11-02) (2007),
  32. 32.
    Rivera, J.E., Durán, F., Vallecillo, A.: A metamodel for Maude,
  33. 33.
    Rivera, J.E., Durán, F., Vallecillo, A.: Formal Specification and Analysis of Domain Specific Models Using Maude. Simulation 85(11-12), 778–792 (2009)CrossRefGoogle Scholar
  34. 34.
    Rivera, J.E., Durán, F., Vallecillo, A.: A Graphical Approach for Modeling Time-Dependent Behavior of DSLs. In: 2009 IEEE Symposium on Visual Languages and Human-Centric Computing, VL/HCC 2009, pp. 51–55. IEEE (2009)Google Scholar
  35. 35.
    Roldán, M., Durán, F.: Dynamic validation of OCL constraints with mOdCL. ECEASST 44 (2011)Google Scholar
  36. 36.
    Soeken, M., Wille, R., Drechsler, R.: Verifying dynamic aspects of UML models. In: Design, Automation and Test in Europe, DATE 2011, pp. 1077–1082. IEEE (2011)Google Scholar
  37. 37.
    Soeken, M., Wille, R., Kuhlmann, M., Gogolla, M., Drechsler, R.: Verifying UML/OCL models using boolean satisfiability. In: Design, Automation and Test in Europe, DATE 2010, pp. 1341–1344. IEEE (2010)Google Scholar
  38. 38.
    Software Technology Group. DresdenOCL,
  39. 39.
    Troya, J., Vallecillo, A.: A rewriting logic semantics for ATL. Journal of Object Technology 10(5), 1–29 (2011)Google Scholar
  40. 40.
    Warmer, J., Kleppe, A.: The Object Constraint Language: Getting Your Models Ready for MDA. Addison-Wesley (2003)Google Scholar
  41. 41.
    Wirsing, M., Knapp, A.: A formal approach to object-oriented software engineering. Theoretical Computer Science 285, 519–560 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  42. 42.
    Zhang, C., Duan, Z.: Specification and verification of UML 2.0 sequence diagrams using event deterministic finite automata. In: Fifth Intl. Conf. on Secure Software Integration and Reliability Improvement, SSIRI 2011, pp. 41–46. IEEE (2011)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Francisco Durán
    • 1
  • Manuel Roldán
    • 1
  • Antonio Moreno
    • 1
  • José María Álvarez
    • 1
  1. 1.Dpto. Lenguajes y Ciencias de la ComputaciónUniversidad de MálagaSpain

Personalised recommendations