Mathematical Programming For Anomaly Analysis Of Clafer Models

Clafer combines UML-like class- and meta-modeling with feature-oriented variability-modeling and first-order logic constraints. The considerable expressiveness of Clafer mainly stems from its built-in variability constructs, multiplicity annotations and recursive model structures which yield a potentially unbounded number of valid model instances. As a result, automated reasoning about semantic properties like model consistency (i.e., existence of valid model instances) and anomalies (e.g., false cardinality bounds) is very challenging. Recent analysis techniques are inherently incomplete as they impose an a-priori finite search space with either manually or heuristically adjusted bounds. In this paper, we present a novel approach for automated search-space restriction for a considerably rich, yet decidable fragment of the Clafer language that guarantees sound and complete detection results for a wide range of semantic anomalies. Our approach employs principles from mathematical programming by encoding Clafer models as Mixed Integer Linear Programs (MILP). Our experimental evaluation shows remarkable improvements of run-time efficiency as well as effectiveness of anomaly detection as compared to existing techniques.