« zurück

Erfolgreiche Verteidigung der Dissertation

Dr. Nils Przigoda

In seiner Dissertation beschäftigte sich Nils Przigoda mit der Validierung und Verifikation von UML/OCL Modellen mit formalen Methoden mit Hilfe von SMT-Beweisern. Hierzu wurde ein allgemeines Verfahren entwickelt, welches UML/OCL Modelle in ein für SMT-Beweiser gültiges Eingangsformat überführt. Dieser Vorgang wird auch als Modelltransformation oder kurz Transformation bezeichnet. Aufbauend hierauf wurden dann verschiedene Verfahren zur Validierung und Verifikation sowohl von strukturellen Eigenschaften als auch von Verhaltensaspekten von UML/OCL Modellen realisiert. Ein struktureller Ansatz ermittelt bei nicht-instanziierbaren Modellen (d.h. Modelle, die widersprüchliche Bedingungen enthalten) alle minimalen Gründe der Widersprüche. Ein anderer Aspekt der Arbeit beschäftigt sich mit der parallelen Ausführung von Methoden. Ferner wird in der Arbeit demonstriert, dass die entwickelten Ansätze auch in einem größeren Feld anwendbar sind. Exemplarisch wird dies anhand von "Timing"-Eigenschaften von MARTE/CCSL Modellen, einem UML2-Profil, demonstriert. Abschließend wird ein Ansatz zum Prüfen von einer gegebenen Implementierung einer Methode gegen die geforderten Eigenschaften auf der Modellebene vorgestellt. Insgesamt können mit den vorgestellten Ansätzen damit bereits vor einer Implementierung mannigfaltige Eigenschaften validiert und verifiziert sowie die Ergebnisse auf die nächsten Ebenen im Systementwurf übertragen werden.

Wir gratulieren!