Viele Beispiele aus Forschung und Industrie sind kleine Systeme und Sandkastenbeispiele, welche über formale Methoden spezifiziert wurden. Bei größeren Systemen stoßen insbesondere Verifikationsverfahren und Theorem-Beweiser an ihre Grenzen. Formale Methoden sollten vor ihrer Verwendung auf Strukturierungsmechanismen, wie Modul, Schichten und Komponentenkonzepte untersucht werden.
Denkbar ist die Verwendung formaler Methoden für kleine Module des Gesamtsystems. Eigenschaften eines Moduls werden spezifiziert und verifiziert, nicht mehr die Gesamtanwendung. Dies wurde beispielsweise von Praxis Critical Systems praktiziert.
Methoden- und Werkzeugkompetenz
Formale Methoden gehören nicht zur Allgemeinbildung von Software-Ingenieuren. Quereinsteiger und Umsteiger haben in der Regel kein Wissen über formale Methoden. In vielen kleinen und mittleren Unternehmen wird die Software-Entwicklung auch von Ingenieuren betrieben, die vor Jahren noch Schaltungen entworfen haben. Methodenwissen ist dort noch im Entstehen. Wissen und Erfahrungen im Umgang mit formalen Methoden müssen im Unternehmen noch gesammelt werden.
Es besteht das Risiko, dass Projekte aus Mangel an Methoden- und Werkzeugwissen scheitern. Dieses Risiko kann über Schulungen und Coaching durch Partner aus spezialisierten Firmen oder aus der Forschung gemindert werden. In einem Pilotprojekt lassen sich Möglichkeiten und Grenzen formaler Methoden für den Anwendungsbereich erkunden.
Eines der Kernelemente einer guten Spezifikation ist ihre Verständlichkeit. Bei formalen Spezifikationen besteht das Risiko, dass diese von den Auftraggebern (dem Kunden) nicht mehr vollständig verstanden wird, da mathematisches Wissen und Methodenwissen nicht vorhanden ist. Die Spezifikation ist nicht mehr reviewfähig und damit nicht mehr validierbar. Auf Kundenseite ist daher ebenso Wissen über formale Methoden erforderlich.
Reifegrad der Werkzeuge
Obwohl es formale Notationen wie Z oder VDM bereits seit über 10 Jahren gibt, sind bislang wenige Werkzeuge für diese Spezifikationssprachen erschienen. Wenige Hersteller und Universitäten bieten Tool-Unterstützungen an. Der Markt für diese Werkzeuge scheint vergleichsweise klein zu sein. Gut unterstützt sind dagegen Verfahren wie das Model Checking oder Statische Analyse.
Einsatz von Fremdkomponenten
Kaum ein Softwareprojekt setzt derzeit direkt auf einer Hardware auf, tatsächlich werden Systeme in Teilen aus zugekauften oder bestehenden Komponenten bzw. Bibliotheken zusammengesetzt. Diese Komponenten sind beispielsweise Betriebssysteme, Netzwerktreiber, Middleware-Schnittstellen, Datenbanksysteme. Der Anwendungskontext entscheidet über die Zahl der Fremdkomponenten.
In einem Gesamtsystem hat jedes Bauteil ein Fehler- bzw. Ausfallrisiko. Fremdkomponenten sind nur mit Aufwand über Abstraktionen in formalen Modellen zu erfassen. Das schwächt die Aussagekraft des formalen Gesamtmodells.
Methodenbruch und Integration in Prozesse
Formale Methoden werden zusammen mit anderen Methoden in einem Entwicklungsprozess verwendet. Wenn diese Methoden und ihre darunter liegenden Modelle nicht zusammenpassen, gibt es Brüche im Entwicklungsprozess. Fehler können sich bei der Modellumsetzung einschleichen und der Aufwand steigt. Wenn eine formale Methode verwendet wird, muss sie sich nahtlos in den Entwicklungsprozess eingliedern und sich auch in Teilprozesse wie beispielsweise das Changemanagement einfügen.