Verification-Driven Slicing of UML/OCL Models

Asadullah Shaikh, Robert Clarisó Viladrosa, Uffe Kock Wiil, Nasrullah Memon

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review


Model defects are a significant concern in the Model-Driven Development (MDD) paradigm, as model transformations and code generation may propagate errors 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. In this paper, we consider a specific static model (UML class diagrams annotated with unrestricted OCL constraints) and a specific property to verify (satisfiability, i.e., “is it possible to create objects without violating any constraint?”).
Current approaches to this problem have an exponential worst-case runtime. We propose a technique to improve their scalability by partitioning the original model into submodels (slices) which can be verified independently and where irrelevant information has been abstracted. The definition of the slicing procedure ensures that the property under verification is preserved after partitioning.
Original languageEnglish
Title of host publication25th IEEE/ACM International Conference on Automated Software Engineering (ASE 2010)
Number of pages10
PublisherAssociation for Computing Machinery
Publication date2010
ISBN (Print)978-1-4503-0116-9
Publication statusPublished - 2010
Event25th IEEE/ACM International Conference on Automated Software Engineering (ASE 2010). - Antwerp, Belgium
Duration: 20. Sep 201024. Sep 2010


Conference25th IEEE/ACM International Conference on Automated Software Engineering (ASE 2010).


Dive into the research topics of 'Verification-Driven Slicing of UML/OCL Models'. Together they form a unique fingerprint.

Cite this