Contradiction Analysis for Inconsistent Formal Models

Modeling languages such as UML or SysML in combination with constraint languages such as OCL allow for an abstract description of a system prior to its implementation. But the resulting system models can be highly non-trivial and, hence, errors in the descriptions can easily arise. In particular, too strong restrictions leading to an inconsistent model are common. Motivated by this, researchers and engineers developed methods for the validation and verification of given formal models. However, while these methods are efficient to detect the existence of an inconsistency, the designer is usually left alone to identify the reasons for it. In this contribution, we propose an automatic method which efficiently determines reasons explaining the contradiction in an inconsistent UML/OCL model. For this purpose, all constraints causing the contradiction are comprehensibly analyzed. By this, the designer is aided during the debugging of his/her model.