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 115
- Downloads 0
Using Real-World Car Traffic Dataset in Vehicular Ad Hoc Network Performance Evaluation
Vehicular ad hoc networking is an emerging paradigm which is gaining much interest with the development of new topics such as the connected vehicle, the autonomous vehicle, and also new high-speed mobile communication te...
An Effective Reasoning Algorithm for Question Answering System
Knowledge representation (KR) is the most desirable area of research to make the system intelligent. Today is the era of knowledge that requires articulations, semantic, syntax etc. These requirements, forced to de...
Implementation of Intelligent Automated Gate System with QR Code
This paper is about QR code-based automated gate system. The aim of the research is to develop and implement a type of medium-level security gate system especially for small companies that cannot afford to install high-t...
Time Varying Back Propagating Algorithm for MIMO Adaptive Inverse Controller
In the field of automatic control system design, adaptive inverse is a powerful control technique. It identifies the system model and controls automatically without having prior knowledge about the dynamics of plant. In...
Revisit of Logistic Regression
Logistic regression (LR) is widely applied as a powerful classification method in various fields, and a variety of optimization methods have been developed. To cope with large-scale problems, an efficient optimization me...