Formale Methoden gibt es viele, die Übersicht in der Formal Methods Virtual Library nennt 92 Methoden und Werkzeuge. Die Auswahl einer geeigneten Spezifikationssprache bzw. –methode ist daher nicht ganz einfach.
Wirtschaftliche Kriterien
Der Wert der entwickelten Software hängt an der formalen Spezifikationssprache, denn die Software kann nur über die Pflege der formalen Spezifikation effektiv weiterentwickelt werden. Die formalen Spezifikationsdokumente haben einen Investitionswert, wie auch der entstandene Code. Wenn die Werkzeuge zur Sprache oder die Sprache selbst von ihrem Hersteller nicht mehr unterstützt werden, ist der Wert der damit entwickelten Software gefährdet. Das Risiko des Support-Verlustes für Werkzeuge und Sprachen ist ein zentrales Entscheidungskriterium.
Referenzprojekte
Die Anwendbarkeit einer formalen Spezifikationssprache ist nicht auf Papierbasis entscheidbar. Referenzprojekte, die in ihren Eigenschaften dem geplanten Projekt entsprechen, sind dagegen ein verlässlicher Anhaltspunkt für die Verwendbarkeit von Werkzeugen und Spezifikationssprachen. Referenzprojekte können beim Hersteller erfragt werden. Ohne Referenzprojekte ist man Beta-Tester für Methodik, Sprache und Werkzeuge.
Support, Beratung und Training
Kaum eine Sprache oder Methodik kann durch reine Lektüre eines Whitepapers und durch die Installation irgendeines Produktes eingeführt werden. Schulungen für Mitarbeiter, Beratung bei den ersten Spezifikationen und Support bei Problemen mit Werkzeugen sind erforderlich. Beratung, Support und Training müssen von einem Hersteller einkaufbar sein. Sprachen und Werkzeuge, zu denen es keinen (käuflichen) Support gibt, sollten nicht verwendet werden.
Werkzeugunterstützung
Werkzeuge machen den Einsatz formaler Spezifikationsmethoden erst möglich, sie erlauben maschinelle Konsistenzüberprüfungen und Analysen der Spezifikation. Sie verstecken über grafische Editoren die formale, mathematische Notation. Damit wird formale Spezifikation für weniger spezifisch ausgebildetes Personal verwendbar.
Ohne (grafische) Werkzeuge wird die Verwendung der formalen Spezifikationssprache komplex, Fehler in der Spezifikation werden wahrscheinlich. Die Mehrwerte der Formalität werden durch höhere Fehlerwahrscheinlichkeit in den Spezifikationen aufgehoben.