Formale Methoden heute – ein sommerlicher Briefwechsel

Mit der Bedeutung Formaler Methoden habe ich mich in den letzten 40 Jahren immer wieder beschäftigt. Im Sommer fand ich eine Arbeit, die für mich einen ziemlichen Durchbruch darstellt. Ich habe mich darüber mit meinem langjährigen Diskussionspartner, Manfred Broy in München, per E-Mail ausgetauscht. Ich möchte diese Korrespondenz allen Lesern dieses Blogs zu Kenntnis bringen – natürlich mit Zustimmung von Herrn Broy.

Am 22.7.2010 schrieb ich an Manfred Broy:

…habe gerade einen Artikel über formale Verifikation gelesen, der mich 100% überzeugt hat. Hätten doch in den letzten 40 Jahren alle Leute so sorgfältig gearbeitet und so sauber argumentiert. Der Artikel ist von Gerwin Klein et al. in den CACM 53,6 (Juni 2010), 107-115. Besonders gefreut hat es mich, dass dabei Herrn Nipkows Isabelle zum Einsatz kam. Gratulation an Ihr Team.

Eine große Einschränkung machen die Autoren. Sie verifizieren kein existierendes Programm, sondern entwickeln ein System neu, und zwar so, dass die Verifikation möglichst leicht wird. Das erinnert mich an die Wette, die Sie Anfang der 1970er Jahre für die Münchner Informatik einzulösen versuchten. Sie verifiziertes damals nicht das ursprüngliche 25 Zeilen lange Textformatierungs­programm von Peter Naur, sondern schrieben ein ganz anderes Programm und stellten dazu einige Korrektheitsbetrachtungen an. Einen formalen Beweis für das ursprüngliche Naur-Programm, das die darin enthaltenen 15 weltbekannten Fehler aufgedeckt hätte, habe ich bis heute noch nicht gesehen.

Das wahre Traumziel der Praxis, ein von einer Fremdfirma gekauftes oder implementiertes Programm anhand seiner Spezifikationen verifizieren zu lassen, wird man in den nächsten 40 Jahren wohl nicht mehr erreichen.

Am 27.7.2010 erhielt ich folgende Antwort von Manfred Broy:

… über Ihre E-Mail habe ich mich aufrichtig gefreut. Ich stimme dem, was Sie schreiben, ganz und gar zu. Formale Methoden haben wirklich enorme Fortschritte gemacht. Wir selbst haben auch praktische Systeme verifiziert. Gerwin Klein ist ein klassisches Gewächs unserer Gruppe, genauer meines Kollegen Tobias Nipkow, der Forschung auf absolutem Weltniveau macht. Mit der Beweistechnologie ISABELLE sind wir Leading Edge. In dem Projekt Verisoft XT sind ähnliche Dinge entstanden, wie Herr Klein sie hier publiziert hat.

  > Eine große Einschränkung machen die Autoren.
  > Sie verifizieren kein existierendes Programm,
  > sondern entwickeln ein System neu, und zwar 
  > so, dass die Verifikation möglichst leicht wird.

Ihre Bemerkung ist natürlich absolut zutreffend. Dahinter verbirgt sich aber ein größeres Problem. So, wie heute in der Regel Software geschrieben wird, wird eine ganze Reihe von Konzepten verwendet, die eben keine sehr klare und durchschaubare logische Struktur mit sich bringen. Das wichtigste Beispiel sind sicher umfangreicher Pointer-Strukturen. Für Programme, die mit solchen Konstrukten verfasst sind, ist eine Verifikation zwar nicht unmöglich, aber ungeheuer aufwändig. Nebenher gesagt, sind solche Programme bzw. Programmkonzepte − wie das schon der Altmeister Dijkstra bemerkt hat – besonders fehleranfällig und damit ganz unabhängig von der Frage der formalen Verifikation nicht ungefährlich.

Heutige Verifikationstechniken, gepaart mit den Möglichkeiten der modellbasierten Entwicklung, rückt Verifikation tatsächlich wieder deutlich näher in den Bereich des praktisch Möglichen. Die Vorstellung, dass umfangreiche Software modellbasiert entwickelt, verifiziert und aus den Modellen der Code generiert wird, ist keine Utopie mehr.

Nachtrag im Februar 2011:

Was ich in meiner ursprünglichen Mail an Herrn Broy weggelassen hatte, war die Befürchtung, dass es den meisten Praktikern heute noch schwer fallen wird, bei einem Programm in der Größenordnung von 9 kLOC allein für die formale Verifikation etwa 20 Personenjahre zu rechtfertigen. Das geht sicherlich nur bei besonders sicherheitsrelevanten Produkten. Ich rechne es den Autoren jedoch hoch an, dass sie realistische Zahlen nennen. Verbesserungen sind bestimmt möglich und werden sich im Laufe der kommenden Jahrzehnte sicherlich auch einstellen.