Verification-Driven Slicing of UML/OCL Models

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

Publikation: Kapitel i bog/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer 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.
Titel25th IEEE/ACM International Conference on Automated Software Engineering (ASE 2010)
Antal sider10
ForlagAssociation for Computing Machinery
ISBN (Trykt)978-1-4503-0116-9
StatusUdgivet - 2010
Begivenhed25th IEEE/ACM International Conference on Automated Software Engineering (ASE 2010). - Antwerp, Belgien
Varighed: 20. sep. 201024. sep. 2010


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


Dyk ned i forskningsemnerne om 'Verification-Driven Slicing of UML/OCL Models'. Sammen danner de et unikt fingeraftryk.