Frank Huch: Model Checking für Erlang Programme -- Abstraktion der kontextfreien Struktur ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Abstract des Vortrags: Ich präsentiere einen Ansatz für die formale Verifikation von Erlang Programmen mittels Model Checking und Abstraktion. Im allgemeinen ist Model Checking für interessante Logiken und Erlang-Programme unentscheidbar. Ich habe ein Framework definiert, in dem es möglich ist dennoch Eigenschaften von Erlang-Programmen zu beweisen. Hierzu muß eine Abstrakten Interpretation definiert werden. Die Abstraktion ist sicher in dem Sinne, daß alle Pfade des ursprünglichen Systems erhalten bleiben. Betrachten wir Formeln, welche auf allen Pfaden eines System gelten sollen, wie z.B. in Linear Time Logic (LTL), so gilt eine Formel, welche im Abstrakten System bewiesen ist, auch im wirklichen System. Für eine große Klasse von Erlang-Programmen und Abstrakten Interpretationen mit endlichem Definitionsbereich, bildet die abstrakte operationelle Semantik ein endliches Transitionssystem. Für dieses kann nun automatisch mittels Model Checking entschieden werden, ob es eine in LTL ausgedrückte Eigenschaft erfüllt. Diese Technik kann leider nicht für beliebige Erlang-Programme verwendet werden, da Erlang eine funktionale Programmiersprache ist. Nicht-endrekursive Funktionsaufrufe in Erlang-Programmen erzeugen auch in der abstrakten operationellen Semantik einen unendlichen Zustandsraum. Dies liegt an der kontextfreien Struktur funktionaler Programmiersprachen. Ich habe deshalb eine Abstraktion dieser kontextfreien Struktur definiert, sodaß die Abstraktion auch für solche Erlang-Programme ein endliches Transitionssystem liefert. Auch diese Abstraktion ist sicher, in dem Sinn, daß alle Pfade des ursprünglichen Systems erhalten bleiben und LTL Formeln beweisen werden können. Viele funktionale Standardfunktionen, wie z.B. die Funktionen length oder append, verwenden nicht-endrekursive Funktionsaufrufe. Deshalb konnte die oben beschriebene Technik zur Verifikation vieler Erlang-Programme nicht eingesetzt werden. In der Abstraktion der kontextfreien Struktur werden Erlang Programme zunächst in eine Graphrepräsentation übersetzt. Hier werden die verschachtelten Aufrufe in einem Call Stack separiert. Nicht- endrekursive Aufrufe werden dann durch Sprünge abstrahiert. Hierbei werden nur rekursive Sprünge abstrahiert. Zwischenberechnungen, welche nur Endrekursion verwenden werden voll expandiert. So erhalten wir eine abstrahierte, endliche Graphrepräsentation des Programms, auf dessen Basis wir dann die abstrakte operationelle Semantik berechnen und zum Model Checking verwenden können. Ein weiterer Vorteil dieser Abstraktion ist eine kompaktere Darstellung der Zustände des Transitionssystems, wodurch wir in der Lage sind mit gleichem Speicher, größere Systeme zu verifizieren. Die vorgestellten Abstraktionen wurden prototypisch implementiert und zur Verifikation einiger Erlang-Programme verwendet.