A Formal Approach to Finding Inconsistencies in a Metamodel

Research output: Contribution to journalArticlepeer-review

Abstract

Checking the consistency of a metamodel involves finding a valid metamodel instance that provably meets the set of constraints that are dened over the metamodel. These constraints are often specified in Object Constraint Language (OCL). Often, a metamodel is inconsistent due to conflicts among the constraints. Existing approaches and tools are typically incapable of pinpointing the conflicting constraints and this makes it difficult for users to debug and x their metamodels. In this paper, we present a formal approach for locating conflicting constraints in inconsistent metamodels. Our approach has four distinct features: (1) users can rank individual metamodel features using their own domain specific knowledge, (2) we transform these ranked features to a weighted maximum satisfiability modulo theories (MaxSMT) problem and solve it to compute the set of maximum achievable features, (3) we pinpoint the conflicting constraints by solving the set cover problem using a novel algorithm, and (4) we have implemented our approach into a fully automated tool called MaxUSE. Our evaluation results, using our assembled set of benchmarks, demonstrate the scalability of our work and that it is capable of efficiently finding conflicting constraints.
Original languageEnglish
JournalSoftware and Systems Modeling
Early online date29 Jan 2021
DOIs
Publication statusPublished - 29 Aug 2021

Fingerprint

Dive into the research topics of 'A Formal Approach to Finding Inconsistencies in a Metamodel'. Together they form a unique fingerprint.

Cite this