UML/OCL class diagrams provide high-level descriptions of software systems. Currently, UML/OCL class diagrams are highly used for code generation through several transformations in order to save time and effort of software developers. Therefore, verification of these class diagrams is essential in order to generate accurate transformations. Verification of UML/OCL class diagrams is a quite challenging task when the input is large (i.e., a complex UML/OCL class diagram). In this paper, we present (1) a benchmark for UML/OCL verification and validation tools, (2) an evaluation and analysis of tools available for verification and validation of UML/OCL class diagrams including the range of UML support for each tool, (3) the problems with efficiency of the verification process for UML/OCL class diagrams, and (4) solution for efficient verification of complex class diagrams. 1. Introduction UML/OCL models are designed in order to provide a high-level description of a software system which can be used as a piece of documentation or as an intermediate step in the software development process. In the context of model-driven development (MDD) and model-driven architecture (MDA), a correct specification is required because the entire technology is based on model transformation. Therefore, if the original model is wrong, this clearly causes a failure of the final software system. Regrettably, verification of a software product is a complex and time-consuming task [1] and that also applies to the analysis of the software models. With increasing model size and complexity, the need for efficient verification methods able to cope with the growing difficulties is ever present, and the importance of UML models has increased significantly [2]. There are formal verification tools for automatically checking correctness properties on models [3–6], but the lack of scalability is usually a drawback. We have considered the static structure diagram that describes the structure of a system, modeled as a UML class diagram. Complex integrity constraints will be expressed in OCL. In this context, the fundamental correctness property of a model is satisfiability. We focus our discussion on the verification of a specific property: satisfiability—“is it possible to create objects without violating any constraints.?” The property is relevant in the sense that many interesting properties; for example, redundancy of an integrity constraint can be expressed in terms of satisfiability [7]. Two different notions of satisfiability can be checked, either weak satisfiability or strong
References
[1]
G. Georg, J. Bieman, and R. B. France, “Using alloy and uml/ocl to specify run-time configuration management: a case study,” in Proceedings of UML Workshop on the Practical UML-Based Rigorous Development Methods, Lecture Notes in Informatics, 2001.
[2]
J. Cabot and R. Clarisó, “UML/OCL verification in practice,” in MoDELS'08, Workshop on Challenges in MDE, 2008.
[3]
A. D. Brucker and B. Wolff, “The hol-ocl book,” 2010, http://www.brucker.ch/ bibliography/download/2006/brucker.ea-hol-ocl-book-2006.pdf.
[4]
J. Cabot, R. Clarisó, and D. Riera, “UMLtoCSP: a tool for the formal verification of UML/OCL models using constraint programming,” in Proceedings of the 22nd International Conference on Automated Software Engineering (ASE '07), pp. 547–548, ACM, 2007.
[5]
M. Gogolla, J. Bohling, and M. Richters, “Validation of uml and ocl models by automatic snapshot generation,” in Proceedings of the 6th International Conference Unified Modeling Language, pp. 265–279, Springer, 2003.
[6]
D. Jackson, “Alloy: a lightweight object modelling notation,” ACM Transactions on Software Engineering and Methodology, vol. 11, no. 2, pp. 266–290, 2002.
[7]
J. Cabot, R. Clarisó, and D. Riera, “Verification of uml/ocl class diagrams using constraint programming,” in Proceedings of the IEEE International Conference on Software Testing Verification and Validation Workshop (ICSTW '08), pp. 73–80, IEEE Computer Society, 2008.
[8]
D. Berardi, D. Calvanese, and G. De Giacomo, “Reasoning on UML class diagrams,” Artificial Intelligence, vol. 168, no. 1-2, pp. 70–118, 2005.
[9]
M. Balaban and A. Maraee, “A UML-based method for deciding finite satisfiability in description logics,” in DL'2008, vol. 353 of CEUR Workshop Proceedings, 2008.
[10]
A. D. Brucker and B. Wolff, “The HOL-OCL book,” Tech. Rep. 525, ETH Zurich, 2006.
[11]
A. Queralt and E. Teniente, “Reasoning on UML class diagrams with OCL constraints,” in ER'2006, vol. 4215 of LNCS, pp. 497–512, Springer, 2006.
[12]
A. Maraee and M. Balaban, “Eficient reasoning about finite satisfiability of UML class diagrams with constrained generalization sets,” in ECMDA-FA'2007, vol. 4530 of LNCS, pp. 17–31, Springer, 2007.
[13]
D. Jackson, Software Abstractions: Logic, Language and Analysis, MIT Press, 2006.
[14]
J. Cabot, R. Clariso, E. Guerra, and J. de Lara, “Verification and validation of declarative model-to-model transformations through invariants,” Journal of Systems and Software, vol. 83, no. 2, pp. 283–302, 2010.
[15]
A. Shaikh, R. Clarisó, U. K. Wiil, and N. Memon, “Verification-driven slicing of uml/ocl models,” in Proceedings of the 25th IEEE/ACM International Conference on Automated Software Engineering (ASE '10), ACM, 2010.
[16]
A. Shaikh, U. K. Wiil, and N. Memon, “Uost: Uml/ocl aggressive slicing technique for eficient verification of models,” in SAM, pp. 173–192, 2010.
[17]
A. D. Brucker and B. Wolff, “Hol-ocl: a formal proof environment for uml/ocl,” in Proceedings of the Fundamental Approaches to Software Engineering Conference (FASE '08), pp. 97–100, 2008.
K. R. Apt and M. G. Wallace, Constraint Logic Programming using ECLiPSe, Cambridge University Press, 2007.
[22]
B. Demuth, “The Dresden OCL toolkit and its role in Information Systems development,” in Proceedings of the 13th International Conference on Information Systems Development (ISD '04), Vilnius, Lithuania, 2004.
M. Gogolla, J. Bohling, and M. Richters, “Validating UML and OCL models in USE by automatic snapshot generation,” Software and Systems Modeling, vol. 4, no. 4, pp. 386–398, 2005.
[25]
MOVA, Mova, 2010, http://maude.sip.ucm.es/mova.
[26]
M. Clavel, M. Egea, and V. T. D. Silva, “Mova: a tool for modeling, measuring and validating uml class diagrams,” 2007.
[27]
M. Clave, F. Durán, S. Eker, et al., “Maude: specification and programming in rewriting logic,” Theoretical Computer Science, vol. 285, no. 2, pp. 187–243, 2002.
[28]
D. J. R. J. A. Stafford and A. L. Wolf, “Chaining: a software architecture depen- dence analysis technique,” Tech. Rep., University of Colorado Department of Computer Science, 1997.
[29]
F. Lanubile and G. Visaggio, “Extracting reusable functions by flow graph-based program slicing,” IEEE Transactions on Software Engineering, vol. 23, no. 4, pp. 246–259, 1997.
[30]
Q. Lu, F. Zhang, and J. Qian, “Program slicing: its improved algorithm and application in verification,” Journal of Computer Science and Technology, vol. 3, no. 1, pp. 29–39, 1988.
[31]
M. Weiser, “Program slicing,” IEEE Transactions on Software Engineering, vol. SE-10, no. 4, pp. 352–357, 1984.
[32]
J. Cabot, R. Clariso, and D. Riera, “Papers and researchers: an example of an unsatisfiable uml/ocl model,” http://gres.uoc.edu/UMLtoCSP/examples/ Papers-Researchers.pdf.
[33]
DBLP, Digital bibliography andy library project, http://guifre.lsi.upc.edu/ DBLP.pdf.
[34]
H. H. Kagdi, J. I. Maletic, and A. Sutton, “Context-free slicing of UML class models,” in Proceedings of the IEEE ICSM International Conference on Software Maintenance (ICSM '05), pp. 635–638, IEEE Computer Society, 2005.
[35]
J.-D. Choi, J. H. Field, G. Ramalingam, and F. Tip, “Method and apparatus for slicing class hierarchies,” http://www.patentstorm.us/patents/ 6179491.html.
[36]
J. H. Bae, K. Lee, and H. S. Chae, “Modularization of the UML metamodel using model slicing,” in ITNG, pp. 1253–1254, IEEE Computer Society, 2008.
[37]
J. T. Lallchandani and R. Mall, “Slicing UML architectural models,” in ACM/SIGSOFT SEN, vol. 33, pp. 1–9, 2008.
[38]
J. Zhao, “Applying slicing technique to software architectures,” CoRR, cs.SE/0105008, 2001.
[39]
T. Kim, Y.-T. Song, L. Chung, and D. T. Huynh, “Dynamic software architecture slicing,” in Proceedings of the 23rd International Computer Software and Applications Conference (COMPSAC '99), pp. 61–66, IEEE Computer Society, 1999.
