Efficient Verification-Driven Slicing of UML/OCL Class Diagrams
Journal Title: International Journal of Advanced Computer Science & Applications - Year 2016, Vol 7, Issue 5
Abstract
Model defects are a significant concern in the Model-Driven Development (MDD) paradigm, as model trans-formations and code generation may propagate errors present in the model to other notations where they are harder to detect and trace. Formal verification techniques can check the correctness of a model, but their high computational complexity can limit their scalability. Current approaches to this problem have an exponential worst-case run time. In this paper, we propose a slicing technique which breaks a model into several independent submodels from which irrelevant information can be abstracted to improve the scalability of the verification process. We consider a specific static model (UML class diagrams annotated with unrestricted OCL constraints) and a specific property to verify (satisfiability, i.e., whether it is possible to create objects without violating any constraints). The definition of the slicing procedure ensures that the property under verification is preserved after partitioning. Furthermore, the paper provides an evaluation of experimental results from a real-world case study.
Authors and Affiliations
Asadullah Shaikh, Uffe Wiil
Keywords
Related Articles
- EP ID EP159543
- DOI 10.14569/IJACSA.2016.070571
- Views 105
- Downloads 0
SVM Classification of Urban High-Resolution Imagery Using Composite Kernels and Contour Information
The classification of remote sensing images has done great forward taking into account the image’s availability with different resolutions, as well as an abundance of very efficient classification algorithms. A number of...
QOS,Comparison of BNP Scheduling Algorithms with Expanded Fuzzy System
Parallel processing is a filed in which different systems run together to save the time of the processing and to increase the performance of the system. It has been also seen that it works somewhat up to the load balanci...
A rule-based Afan Oromo Grammar Checker
Natural language processing (NLP) is a subfield of computer science, with strong connections to artificial intelligence. One area of NLP is concerned with creating proofing systems, such as grammar checker. Grammar check...
Breast Cancer Classification using Global Discriminate Features in Mammographic Images
Breast cancer has become a rapidly prevailing disease among women all over the world. In term of mortality, it is considered to be the second leading cause of death. Death risk can be reduced by early stage detection, f...
Insights on Error-Resilient Image Transmission Schemes on Wireless Network
Usage of image as data (or signal) is quite frequent in majority of the user-centric application. However, transmission of image over non-concrete communication medium like air is still vulnerable due to inherent weaknes...