Formale Verifikation von UML-basierten Spezifikationen

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, z.B. 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 Nutze machen. Es wird illustriert, welche Fehler bereits früh in der Entwicklung auftreten können und welche Methoden sich zu deren automatischer Erkennung einsetzen lassen.