Ausführbare Spezifikationen

Eine System für ausführbare Spezifikationen besteht aus zwei Teilen:

  • Einer formalen Spezifikation und
  • der eigentlichen ausführbaren Spezifikation.

Die formale Spezifikation beschreibt Regeln, die für das Softwaresystem gelten sollen. Die Regeln dienen einerseits als Dokumentation der Anforderungen, andererseits können sie formal verifiziert werden, um funktionale Eigenschaften zu garantieren. Dieses Vorgehen legt den Grundstein für höchste Sicherheit.

Das System stellt zudem eine domainspezifische Sprache (DSL) bereit, die Domainexperten dazu dient, ausführbare Spezifikationen zu erstellen. So bringen Experten ihr Fachwissen unmittelbar ein. Das führt zu einer niedrigeren Fehlerquote und damit zu Kostenersparnis bei der Fehlersuche.

Die ausführbare Spezifikation gehorcht den Regeln, die durch die formale Spezifikation etabliert wurden. Die Sicherheit des Softwaresystems wird dadurch erhöht. Wurde eine Verifikation durchgeführt, kann formale Korrektheit auch auf Seiten der ausführbaren Spezifikation garantiert werden. Eine direkte Ausführung ist natürlich möglich. Die ausführbare Spezifikation ist damit auch ein Prototyp.

Zudem besteht die Möglichkeiten zur Code-Generierung in beliebige Sprachen (z.B. C/C++ oder Java). Der Code kann entweder auf sichere Weise erzeugt werden oder mittels Unit-Testing gegen den Prototypen geprüft werden.

Ausführbare Spezifikationen erlauben auch Visualisierung und Fehler-Highlightening, wie es aus der modellbasierten Entwicklung bekannt ist. Dokumentation kann ebenfalls erzeugt werden.

Alle eingesetzten Tools sind Open Source. Zusammen mit dem Einsatz funktionaler Programmierung ist es auch für mittelständische Unternehmen möglich, Software mit höchsten Qualitätsansprüchen zu verwenden.