Entwurfsmustergesteuerte Erzeugung von OCL-Constraints

Eine der grosten Hurden auf dem Weg zur formalen Verifikation von Software ist die Erstellung und Validierung der hierfur notwendigen formalen Spezifikation. Der Erfolg formaler Methoden bei der industriellen Softwareerstellung hangt also davon ab, ob es zum einen gelingt, die notwendigen Zugangsvoraussetzungen fur die Erstellung und Verwendung formaler Objekte gering genug zu machen, und zum anderen davon, formale und informelle Softwaremodelle moglichst eng zu integrieren. Fur letzteres bietet die weithin verwendete, objektorientierte Modellierungssprache Unified Modeling Language (UML) einen guten Ansatzpunkt durch ihre semi-formale Untersprache Object Constraint Language (OCL). In der vorliegenden Arbeit zeigen wir, das es auch fur Programmierer ohne formalen Hintergrund prinzipiell moglich ist, formale Teilspezifikationen in OCL zu erstellen. Dies erfolgt durch Auswahl, Instanziierung und Adaption von schematischen OCL-Constraints, die von Spezialisten sorgfaltig definiert wurden. Durch die Bindung von OCL-Constraints an Entwurfsmuster wird ein hoher Grad an moglicher Hilfestellung und maschineller Unterstutzung erreicht. Durch die Erhebung der Constraints im Rahmen eines konkreten Industrieprojekts wird der Praxisbezug des Ansatzes sichergestellt.