%0 Journal Article
%T Evaluation of Tools and Slicing Techniques for Efficient Verification of UML/OCL Class Diagrams
%A Asadullah Shaikh
%A Uffe Kock Wiil
%A Nasrullah Memon
%J Advances in Software Engineering
%D 2011
%I Hindawi Publishing Corporation
%R 10.1155/2011/370198
%X 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¨C6], 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
%U http://www.hindawi.com/journals/ase/2011/370198/