Um die steigende Komplexität heutiger Softwaresysteme mit Modell-basierten Ansätzen zu beherrschen, hat sich die Unified Modeling Language (UML) zusammen mit der Object Constraint Language (OCL) zu einem de-facto Standard herausgebildet. UML/OCL ermöglicht die Beschreibung von Anforderungen an Verhalten und Struktur komplexer Systeme ohne dabei konkrete Implementierungsdetails zu verlangen. Gleichzeitig wird damit ermöglicht, die Korrektheit der spezifizierten Systeme bereits vor der Implementierung zu prüfen.
Entsprechend wurde in den vergangenen Jahren eine Vielzahl an Verfahren zur Validation und Verifikation von UML/OCL-Modellen vorgestellt. Bisher wurden dabei aber vornehmlich fokussierte Aspekte wie z. B. einzelne Verifikationsaufgaben oder bestimmte UML/OCL-Beschreibungsmittel einzeln betrachtet. Praktisch relevante Systeme werden aber mit einer Vielzahl von Beschreibungsmitteln modelliert, die aufeinander aufbauen und sich gegenseitig ergänzen. Weiterhin wurden die verwendeten Beweistechnologien bisher in der Regel unabhängig voneinander betrachtet – unterschiedliche Vorteile von Beweisern je nach Verifikationsaufgabe konnten daher nicht ausgenutzt werden. Aus diesen Gründen haben sich generelle Verfahren zur Validation und Verifikation in kommerziellen Entwicklungswerkzeugen kaum durchgesetzt.
Im Rahmen des Projektes sollen diese Probleme adressiert werden. Im Fokus steht dabei die Entwicklung eines generischen Frameworks zur Verifikation von UML/OCL-Modellen, welches (1) auf automatischen Beweistechnologien basiert, (2) die Kombination verschiedener UML-Beschreibungsmittel und Verifikationsaufgaben unterstützt und (3) einen einfachen Austausch der zugrunde liegenden Beweistechnologien ermöglicht. Um dies zu erreichen, soll nicht mehr jede einzelne Kombination aus UML-Beschreibungsmittel und Verifikationsaufgabe einzeln formuliert werden. Stattdessen sollen UML-Modelle und Verifikationsaufgaben in äquivalente Basismodelle transformiert werden, welche ausdrucksstark genug sind, um mannigfaltige UML/OCL-Beschreibungsmittel repräsentieren zu können, gleichzeitig aber atomar sind, um die weitere Verarbeitung im Sinne der Validation und Verifikation möglichst einheitlich und flexibel zu gestalten.
