Publikation

Formale Verifikation von UML-basierten Spezifikationen - Prüfung der Korrektheit von Systementwürfen vor deren Implementierung

Mathias Soeken, Robert Wille, Rolf Drechsler

In: Industrie Management - Zeitschrift für industrielle Geschäftsprozesse 01/2013 Seiten 44-48 GITO 2013.

Abstrakt

Der Entwurf komplexer Systeme startet in der Regel mit der Erstellung einer natürlichsprachlichen Spezifikation, aus der im Anschluss die gewünschte Implementierung generiert wird. Um der steigenden Komplexität rechnung zu tragen, werden Spezifikationen darüber hinaus aber auch vermehrt durch formalere Beschreibungen, zum Beispiel mithilfe der Unified Modeling Language (UML) und der Object Constraint Language (OCL) erweitert. Diese ermöglichen es bereits vor der Implementierung die Korrektheit und Widerspruchsfreiheit des spezifizierten Systems zu prüfen. In diesem beitrag werden Verfahren vorgestellt, welche sich diese Möglichkeiten zu Nutzen machen. Es wird illustriert, welche Fehler bereits früh in der Entwicklung auftreten können und welche Methoden sich zu deren automatischer Erkenung einsetzen lassen.

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence