Towards a Developer-Oriented Process for Verifying Behavioral Properties in UML and OCL Models

  • Khanh-Hoang DoanEmail author
  • Martin Gogolla
  • Frank Hilken
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9946)


Validation and verification of models in the software development design phase have a great potential for general quality improvement within software engineering. A system modeled with UML and OCL can be checked thoroughly before performing further development steps. Verifying not only static but also dynamic aspects of the model will reduce the cost of software development. In this paper, we introduce an approach for automatic behavioral property verification. An initial UML and OCL model will be enriched by frame conditions and then transformed into a (so-called) filmstrip model in which behavioral characteristics can be checked. The final step is to verify a property, which can be added to the filmstrip model in form of an OCL invariant. In order to make the process developer-friendly, UML diagrams can be employed for various purposes, in particular for formulating the verification task and the verification result.


Validation and verification Model testing UML and OCL model Behavior property verification 


  1. 1.
    Borgida, A., Mylopoulos, J., Reiter, R.: On the frame problem in procedure specifications. IEEE Trans. Softw. Eng. 21(10), 785–798 (1995)CrossRefGoogle Scholar
  2. 2.
    Cabot, J., Clarisó, R., Riera, D.: UMLtoCSP: a tool for the formal verification of UML/OCL models using constraint programming. In: Proceedings of the Twenty-second IEEE/ACM International Conference on Automated Software Engineering, pp. 547–548, ASE 2007, NY, USA. ACM, New York (2007)Google Scholar
  3. 3.
    Cabot, J., Gogolla, Martin: 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). doi: 10.1007/978-3-642-30982-3_3 CrossRefGoogle Scholar
  4. 4.
    Dan, C., Mihai, P., Adrian, C., Cristian, B., Sorin, M.: Ensuring UML models consistency using the OCL environment. Electron. Notes Theor. Comput. Sci. 102, 99–110 (2004). Proceedings of the Workshop, OCL 2.0 - Industry Standard or Scientific Playground?CrossRefGoogle Scholar
  5. 5.
    Demuth, B., Wilke, C.: Model and object verification by using Dresden OCL. In: Russian-German WS Innovation Information Technologies: Theory and Practice (2009)Google Scholar
  6. 6.
    Doan, K.H., Gogolla, M., Hilken, F.: Addendum to a complete process for behavioral properties verification. University of Bremen, Technical report (2016).
  7. 7.
    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)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Gogolla, M., Hamann, L., Hilken, F., Kuhlmann, M., France, R.: From application models to filmstrip models: an approach to automatic validation of model dynamics. In: Modellierung (MODELLIERUNG 2014) (2014)Google Scholar
  9. 9.
    Gogolla, M., Kuhlmann, M., Hamann, L.: Consistency, independence and consequences in UML and OCL models. In: Dubois, C. (ed.) Tests and Proofs. LNCS, vol. 5668, pp. 90–104. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  10. 10.
    Hilken, F., Hamann, L., Gogolla, M.: Transformation of UML and OCL models into filmstrip models. In: Di Ruscio, D., Varró, D. (eds.) Theory and Practice of Model Transformations. LNCS, vol. 8568, pp. 170–185. Springer International Publishing, Heidelberg (2014)Google Scholar
  11. 11.
    Kosiuczenko, P.: Specification of invariability in OCL. Softw. Syst. Model. 12(2), 415–434 (2011)CrossRefGoogle Scholar
  12. 12.
    Krieger, M.P., Knapp, A., Wolff, B.: Automatic and efficient simulation of operation contracts. In: Proceedings of the Ninth International Conference on Generative Programming and Component Engineering, GPCE 2010, pp. 53–62, NY, USA. ACM, New York (2010)Google Scholar
  13. 13.
    Kuhlmann, M., Gogolla, M.: Modeling and validating mondex scenarios described in UML and OCL with USE. Formal Aspects Comput. 20(1), 79–100 (2007)CrossRefGoogle Scholar
  14. 14.
    Niemann, P., Hilken, F., Gogolla, M., Wille, R.: Extracting frame conditions from operation contracts. In: ACM/IEEE 18th International Conference on Model Driven Engineering Languages and Systems (MoDELS 2015) (2015)Google Scholar
  15. 15.
    Object Management Group - OMG: Unified Modeling Language Specification, version 2.5 (2013).
  16. 16.
    Richters, M., Gogolla, M.: Validating UML models and OCL constraints. In: Evans, A., Kent, S., Selic, B. (eds.) UML 2000 The Unified Modeling Language. LNCS, vol. 1939, pp. 265–277. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  17. 17.
    Shen, W., Compton, K., Huggins, J.: A toolset for supporting UML static and dynamic model checking. In: 2002 Proceedings of 26th Annual International on Computer Software and Applications Conference, COMPSAC 2002 , pp. 147–152 (2002)Google Scholar
  18. 18.
    Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: Grumberg, O., Huth, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 4424, pp. 632–647. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  19. 19.
    Ziemann, P., Gogolla, M.: Validating OCL specifications with the USE tool: an example based on the BART case study. Electron. Notes Theor. Comput. Sci. 80, 157–169 (2003). Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2003)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG 2016

Authors and Affiliations

  • Khanh-Hoang Doan
    • 1
    Email author
  • Martin Gogolla
    • 1
  • Frank Hilken
    • 1
  1. 1.Computer Science DepartmentUniversity of BremenBremenGermany

Personalised recommendations