J. Thees, R. Gotzhein

• Formale Beschreibungstechniken (FDTs) erlauben durch ihre formale Syntax und Semantik eine präzise Systembeschreibung und sind Grundlage für die formale Verifikation. Bei der Implementierung von Systemen wird jedoch nach wie vor von Hand implementiert, selbst wenn ausgereifte Werkzeuge zur automatischen Generierung von Kode direkt aus der formalen Spezifikation existieren. Die Ursache dafür liegt in dem Ruf dieser Werkzeuge, Kode mit extrem geringer Leistungsfähigkeit zu erzeugen. Es gibt jedoch kaum quantitative Leistungsvergleiche zwischen manuell und automatisch generierten Implementierungen, die dieses Vorurteil stützen oder widerlegen könnten. In diesem Beitrag wird ein solcher Leistungsvergleich anhand des Hochleistungsprotokolls XTP und der FDT Estelle vorgestellt. Er liefert eine Bestandsaufnahme des momentanen Entwicklungsstandes bei der automatischen Generierung von Kode aus Estelle-Spezifikationen im direkten Vergleich zu gut optimierten Handimplementierungen. Es zeigt sich, daß in dem betrachteten Fall eines komplexen Protokolls die Handimplementierung zwar merklich leistungsstärker ist. Dieser Leistungsvorteil wird jedoch durch einen sehr hohen Implementierungsaufwand sowie die Schwierigkeit, die Korrektheit bzgl. der Spezifikation sicherzustellen, erkauft. Im einzelnen Anwendungsfall kann es daher trotz der Leistungseinbußen durchaus vorteilhaft sein, automatisch Kode zu erzeugen, zumal in der Bestandsaufnahme festgestellt wurde, daß automatisch generierte Implementierungen z.T. besser abschneiden als erwartet. Zudem besteht - anders als bei der bereits umfassend optimierten Handimplementierung - noch ein erhebliches ungenutztes Potential zur Leistungsverbesserung der automatisch generierten Implementierung.