Leveraging the analysis for invariant independence in formal system models

Formal models, based on modeling languages such as UML in combination with constraint languages such as OCL, allow for an abstract description of a system prior to its implementation. But since the resulting models are often rather complex, redundancies in terms of model descriptions which can directly be implied from already existing constraints can easily arise. In particular, OCL invariants are affected by this. In order to efficiently detect those, methodologies for the analysis for invariant dependence have recently been proposed. However, they have severe limitations with respect to scalability, automation, and quality of the determined results. In this work, we aim for leveraging the analysis for invariant independence in formal systems models by addressing these drawbacks. For this purpose, a new methodology based on the exploitation of powerful solving engines as well as a complete analysis scheme is proposed. Experimental evaluations confirm that the proposed solution is significantly faster and leads to a much better quality of the results.