Skip to main content
Springer Nature Link
Log in

Formulating Model Verification Tasks Prover-Independently as UML Diagrams

  • Conference paper
  • First Online:
Modelling Foundations and Applications (ECMFA 2017)

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

Included in the following conference series:

Abstract

The success of Model-Driven Engineering (MDE) relies on the quality of the employed models. Thus, quality assurance through validation and verification has a tradition within MDE. But model verification is typically done in the context of specialized approaches and provers. Therefore, verification tasks are expressed from the viewpoint of the chosen prover and approach requiring particular expertise and background knowledge. This contribution suggests to take a new view on verification tasks that is independent from the employed approach and prover. We propose to formulate verifications tasks in terms of the used modeling language itself, e.g. with UML and OCL. As prototypical example tasks we show how (a) questions concerning model consistency can be expressed with UML object diagrams and (b) issues regarding state reachability can be defined with UML sequence diagrams.

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
$34.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)
eBook
USD 39.99
Price excludes VAT (USA)
Softcover Book
USD 54.99
Price excludes VAT (USA)

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

References

  1. Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: UML2Alloy: a challenging model transformation. In: Engels, G., Opdyke, B., Schmidt, D.C., Weil, F. (eds.) MODELS 2007. LNCS, vol. 4735, pp. 436–450. Springer, Heidelberg (2007). doi:10.1007/978-3-540-75209-7_30

    Chapter  Google Scholar 

  2. Arshad, F., Mehmood, H., Raza, F., Hasan, O.: g-HOL: a graphical user interface for the HOL proof assistant. In: Artho, C., Ölveczky, P.C. (eds.) FTSCS 2015. CCIS, vol. 596, pp. 265–269. Springer, Cham (2016). doi:10.1007/978-3-319-29510-7_16

    Chapter  Google Scholar 

  3. Awad, A., Sakr, S.: On efficient processing of BPMN-Q queries. Comput. Ind. 63(9), 867–881 (2012)

    Article  Google Scholar 

  4. Balaban, M., Maraee, A., Sturm, A., Jelnov, P.: A pattern-based approach for improving model quality. Softw. Syst. Model. 14(4), 1527–1555 (2015)

    Article  Google Scholar 

  5. Ballis, D., Baruzzo, A., Comini, M.: A minimalist visual notation for design patterns and antipatterns. In: 5th International Conference on Information Technology: New Generations (ITNG 2008), pp. 51–56 (2008)

    Google Scholar 

  6. Beckert, B., Grebing, S.: Evaluating the usability of interactive verification systems. In: Proceedings of 1st International Workshop Comparative Empirical Evaluation of Reasoning Systems, pp. 3–17 (2012)

    Google Scholar 

  7. Bottoni, P., Guerra, E., de Lara, J.: A language-independent and formal approach to pattern-based modelling with support for composition and analysis. Inf. Softw. Technol. 52(8), 821–844 (2010)

    Article  Google Scholar 

  8. 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). doi:10.1007/978-3-540-78743-3_8

    Chapter  Google Scholar 

  9. Cabot, J., Clarisó, R., Riera, D.: Verification of UML/OCL class diagrams using constraint programming. In: First International Conference on Software Testing Verification and Validation, ICST 2008, pp. 73–80. IEEE Computer Society (2008)

    Google Scholar 

  10. Choppy, C., Klai, K., Zidani, H.: Formal verification of UML state diagrams: a petri net based approach. Softw. Eng. Notes 36(1), 1–8 (2011)

    Article  Google Scholar 

  11. Gogolla, M., Büttner, F., Richters, M.: USE: a UML-based specification environment for validating UML and OCL. Sci. Comput. Program. 69, 27–34 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  12. Gogolla, M., Hilken, F.: Model validation and verification options in a contemporary UML and OCL analysis tool. In: Oberweis, A., Reussner, R. (eds.) Proceedings of Modellierung (MODELLIERUNG 2016). LNI, GI, vol. 254, pp. 203–218 (2016)

    Google Scholar 

  13. 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). doi:10.1007/978-3-642-02949-3_8

    Chapter  Google Scholar 

  14. Hilken, F., Hamann, L., Gogolla, M.: Transformation of UML and OCL models into filmstrip models. In: Ruscio, D., Varró, D. (eds.) ICMT 2014. LNCS, vol. 8568, pp. 170–185. Springer, Cham (2014). doi:10.1007/978-3-319-08789-4_13

    Google Scholar 

  15. Hilken, F., Niemann, P., Gogolla, M., Wille, R.: Filmstripping and unrolling: a comparison of verification approaches for UML and OCL behavioral models. In: Seidl, M., Tillmann, N. (eds.) TAP 2014. LNCS, vol. 8570, pp. 99–116. Springer, Cham (2014). doi:10.1007/978-3-319-09099-3_8

    Google Scholar 

  16. Hilken, F., Niemann, P., Gogolla, M., Wille, R.: Towards a catalog of structural and behavioral verification tasks for UML/OCL models. In: Oberweis, A., Reussner, R. (eds.) Proceedings of Modellierung (MODELLIERUNG 2016). LNI, GI, vol. 254, pp. 115–122 (2016)

    Google Scholar 

  17. Homik, M., Meier, A.: Designing a GUI for proofs - evaluation of an HCI experiment. CoRR abs/0903.3926 (2009)

    Google Scholar 

  18. Lam, V.S.W.: A formalism for reasoning about UML activity diagrams. Nordic J. Comp. 14(1), 43–64 (2007)

    MathSciNet  MATH  Google Scholar 

  19. Lapets, A., Kfoury, A.J.: A user-friendly interface for a lightweight verification system. Electr. Notes Theor. Comput. Sci. 285, 29–41 (2012)

    Article  MATH  Google Scholar 

  20. Lüth, C.: User interfaces for theorem provers: necessary nuisance or unexplored potential? ECEASST 23 (2009). http://dblp.uni-trier.de/db/journals/eceasst/eceasst23.html

  21. Moisuc, D., Revol, S., Snook, C.F.: UML user interface to a proof-based hardware design flow. In: Forum on Specification and Design Languages, FDL 2006, pp. 337–344. ECSI (2006)

    Google Scholar 

  22. Pescador, A., Garmendia, A., Guerra, E., Cuadrado, J.S., de Lara, J.: Pattern-based development of domain-specific modelling languages. In: 18th ACM/IEEE MoDELS 2015, pp. 166–175 (2015)

    Google Scholar 

  23. Remenska, D., Willemse, T.A.C., Templon, J., Verstoep, K., Bal, H.: Property specification made easy: harnessing the power of model checking in UML designs. In: Ábrahám, E., Palamidessi, C. (eds.) FORTE 2014. LNCS, vol. 8461, pp. 17–32. Springer, Heidelberg (2014). doi:10.1007/978-3-662-43613-4_2

    Chapter  Google Scholar 

  24. Salay, R., Chechik, M.: A generalized formal framework for partial modeling. In: Egyed, A., Schaefer, I. (eds.) FASE 2015. LNCS, vol. 9033, pp. 133–148. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46675-9_9

    Google Scholar 

  25. Salay, R., Chechik, M., Famelis, M., Gorzny, J.: A methodology for verifying refinements of partial models. J. Object Technol. 14(3), 3:1–3:31 (2015)

    Article  Google Scholar 

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

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

  28. 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). doi:10.1007/978-3-642-21470-7_6

    Chapter  Google Scholar 

  29. Wang, X., Rutle, A., Lamo, Y.: Towards user-friendly and efficient analysis with alloy. In: Model-Driven Engineering, Verification and Validation, MoDeVVa@MoDELS 2015, pp. 28–37 (2015)

    Google Scholar 

  30. Zloof, M.M.: QBE/OBE: a language for office and business automation. IEEE Comput. 14(5), 13–22 (1981)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Bremen, Bremen, Germany

    Martin Gogolla & Frank Hilken

  2. Cyber-Physical Systems, DFKI GmbH, Bremen, Germany

    Philipp Niemann & Robert Wille

  3. Johannes Kepler University, Linz, Austria

    Robert Wille

Authors
  1. Martin Gogolla
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Frank Hilken
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Philipp Niemann
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Robert Wille
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Martin Gogolla .

Editor information

Editors and Affiliations

  1. University of Paderborn, Paderborn, Germany

    Anthony Anjorin

  2. Tecnalia Research and Innovation, Derio, Spain

    Huáscar Espinoza

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Gogolla, M., Hilken, F., Niemann, P., Wille, R. (2017). Formulating Model Verification Tasks Prover-Independently as UML Diagrams. In: Anjorin, A., Espinoza, H. (eds) Modelling Foundations and Applications. ECMFA 2017. Lecture Notes in Computer Science(), vol 10376. Springer, Cham. https://doi.org/10.1007/978-3-319-61482-3_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-61482-3_14

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-61481-6

  • Online ISBN: 978-3-319-61482-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation