Entwurfsmustergesteuerte Erzeugung von OCL-Constraints


Autoren: Thomas Baar, Reiner Hähnle, Theo Sattler, Peter H. Schmitt


-------------------------------------------------------------------------



  Eine der größten Hürden auf dem Weg zur formalen Verifikation von
  Software ist die Erstellung und Validierung der hierfür notwendigen
  formalen Spezifikation.  Der Erfolg formaler Methoden bei der
  industriellen Softwareerstellung hängt also davon ab, ob es zum
  einen gelingt, die notwendigen Zugangsvoraussetzungen für die
  Erstellung und Verwendung formaler Objekte gering genug zu machen,
  und zum anderen davon, formale und informelle Softwaremodelle
  möglichst eng zu integrieren.  Für 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, daß es auch für Programmierer ohne formalen
  Hintergrund prinzipiell möglich ist, formale Teilspezifikationen in
  OCL zu erstellen.  Dies erfolgt durch Auswahl, Instanziierung und
  Adaption von schematischen OCL-Constraints, die von Spezialisten
  sorgfältig definiert wurden.  Durch die Bindung von OCL-Constraints
  an Entwurfsmuster wird ein hoher Grad an möglicher
  Hilfestellung und maschineller Unterstützung erreicht. Durch die
  Erhebung der Constraints im Rahmen eines konkreten Industrieprojekts
  wird der Praxisbezug des Ansatzes sichergestellt.