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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
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
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
Awad, A., Sakr, S.: On efficient processing of BPMN-Q queries. Comput. Ind. 63(9), 867–881 (2012)
Balaban, M., Maraee, A., Sturm, A., Jelnov, P.: A pattern-based approach for improving model quality. Softw. Syst. Model. 14(4), 1527–1555 (2015)
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)
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)
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)
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
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)
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)
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)
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)
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
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
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
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)
Homik, M., Meier, A.: Designing a GUI for proofs - evaluation of an HCI experiment. CoRR abs/0903.3926 (2009)
Lam, V.S.W.: A formalism for reasoning about UML activity diagrams. Nordic J. Comp. 14(1), 43–64 (2007)
Lapets, A., Kfoury, A.J.: A user-friendly interface for a lightweight verification system. Electr. Notes Theor. Comput. Sci. 285, 29–41 (2012)
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
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)
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)
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
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
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)
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)
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)
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
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)
Zloof, M.M.: QBE/OBE: a language for office and business automation. IEEE Comput. 14(5), 13–22 (1981)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights 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)