Mathematical Programming for Anomaly Analysis of Clafer Models
| Autor: | Michael Ries, Andy Schürr, Markus Weckesser, Malte Lochau |
|---|---|
| Rok vydání: | 2018 |
| Předmět: |
Mathematical optimization
Computer science 0202 electrical engineering electronic engineering information engineering 020207 software engineering 020201 artificial intelligence & image processing Anomaly detection Recursive model 02 engineering and technology Semantic property Automated reasoning Decidability |
| Zdroj: | MoDELS |
| DOI: | 10.1145/3239372.3239398 |
| Popis: | 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 runtime efficiency as well as effectiveness of anomaly detection as compared to existing techniques. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|