Formale Methoden wenden mathematische Arbeitsweisen – wie Modellbildung oder das Beweisen wesent-licher Eigenschaften solcher Modelle – auf den Entwurf technischer Systeme an. Das Teilgebiet der formalen Verifikation beschäftigt sich mit dem Beweisen von Eigenschaften wichtiger Modelle. Als besonders wichtig gelten Endliche Automaten, denn diese beschreiben das Verhalten von Software- oder Hardwareimplemen-tierungen diskreter Steuerungen und damit von Schlüsselfunktionalität fast aller technischen Systeme.
Einführend wird der Stand der Kunst des Model Checking erläutert. Technischer Kern des Vortrags ist ein wesentlich anwendungsspezifischeres Verfahren, das durch ein VHDL-Programm beschriebenes Verhalten einer digitalen Schaltung lückenlos und automatisch mit einem abstrakten Automaten, einem abstrakten VHDL, vergleicht. Abstraktes VHDL ist eine Feinspezifikation der Schaltung durch ihre Operationen. Operationen formalisieren i.A. kurze Schaltungsaktivitäten wie Lese- oder Schreibzugriffe, Instruktionen oder Arbitrierungs-zyklen. Es wird erläutert, wie abstraktes VHDL erstellt, bezüglich der Grobspezifikation verifiziert, und dann mit dem VHDL automatisch verglichen wird. Dieser Vergleich zeigt Fehler in der Implementierung der Operationen an sowie Diagnosen zu ihrer Behebung. Automatische Überprüfung eines Kriteriums zur vollständigen Erfassung der Schaltungsfunktionalität durch Operationen garantiert Korrektheit des Codes.
Es folgt eine kurze Darstellung der Anwendungs- und Prozessseite des Themas: Die operationsbasierte formale Schaltungsverifikation wurde in der zentralen Siemensforschung vor fast 20 Jahren konzipiert, bei Siemens, Infineon und weiteren Chipherstellern erprobt und schließlich in dem Spin-Off OneSpin Solutions zur Produkt-reife geführt. Der Ansatz garantierte Korrektheit zahlreicher VHDL-Programme einer Größenordnung von 100000 LoC – ein prominentes Beispiel ist der in der Automobilelektronik weit verbreitete TriCore-Prozessor von Infineon. Obwohl die Verifikationsproduktivität des Ansatzes mit der der simulationsbasierten Verifikation vergleichbar ist und auch „Nichtformalisten“ die Technik erfolgreich erlernen können, hat sich der Ansatz noch nicht in der Breite durchgesetzt. Auch die Übertragbarkeit des Erfolgsrezepts der operationsbasierten Modellierung auf andere Anwendungsbereiche wie die Fertigungstechnik wurde bisher kaum untersucht.
Der Vortrag schließt mit der Analyse der Erfolgsfaktoren für den Breiteneinsatz der operationsbasierten Schal-tungsverifikation und schildert mögliche nächste Schritte. Vielversprechend erscheint eine weitere Nutzung von abstraktem VHDL für die funktionale Sicherheitsanalyse einer Schaltung. Während Verifikation Entwurfs-fehler aufspürt, beschäftigt sich die Sicherheitsanalyse mit zufälligen Fehlern, verursacht etwa durch Alterungs-prozesse oder durch Strahlungseinflüsse, und so möglichen schwerwiegenden Systemausfällen. Es wird skizziert, wie mithilfe des abstrakten VHDL eine Sicherheitsanalyse für Schaltungen konzipiert und so eine Brücke zwischen formaler Verifikation und funktionaler Sicherheitsanalyse geschlagen wurde.
Kurz-Bio: Wolfram Büttner promovierte 1978 in Mathematik an der Tulane University in New Orleans, habilitierte in diesem Fach an der TU Darmstadt und wechselte dann in die Informatik. Seit 1989 ist er Außerplanmäßiger Professor an der TU Kaiserslautern. Von 1984 bis 2002 arbeitete Dr. Büttner in den Corporate Technology Labs (CT) von Siemens in München – zuletzt als Abteilungsdirektor mit Verantwortung für die Themengebiete formale Methoden, diskrete und stochastische Optimierung sowie Lernende Systeme. Seit 2000 fokussierte Dr. Büttner seine Tätigkeit auf die formale Schaltungsverifikation und führte die Verifikationstechnologie von CT zur Produktreife und auf den canadian pharmacy no prescription Markt – erst bei Infineon und ab 2005 in zwei Start-Up’s.
