Verification of Erlang programs using abstract interpretation and model checking

Huch, Frank Günter; Indermark, Klaus

doi:urn:nbn:de:hbz:82-opus-4303

Verification of Erlang programs using abstract interpretation and model checking

Huch, Frank Günter (Author)

2001 & 2002

Verantwortlichkeitsangabevorgelegt von Frank Günter Huch

ImpressumAachen : Publikationsserver der RWTH Aachen University 2001

UmfangX, 148 S.

Aachen, Techn. Hochsch., Diss., 2001

Prüfungsjahr: 2001. - Publikationsjahr: 2002

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Indermark, Klaus (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2001-11-02

Online
URN: urn:nbn:de:hbz:82-opus-4303
URL: https://publications.rwth-aachen.de/record/59420/files/02_170.pdf

Einrichtungen

Fakultät für Mathematik, Informatik und Naturwissenschaften (100000)

Inhaltliche Beschreibung (Schlagwörter)
Informatik (frei) ; Verteiltes System (frei) ; Softwareentwicklung (frei) ; Funktionale Programmiersprache (frei) ; Programmverifikation (frei) ; Model checking (frei) ; Abstrakte Interpretation (frei) ; Erlang (frei) ; Verification (frei) ; Model Checking (frei) ; Abstraction (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Die Funktionale Programmiersprache Erlang wird erfolgreich zur Entwicklung Verteilter Systeme eingesetzt. Wir präsentieren einen Ansatz zur formalen Verifikation von Erlang Programmen mittels abstrakter Interpretation und Model Checking. Im allgemeinen ist Model Checking für Temporallogiken und Erlangprogramme unentscheidbar. Deshalb definieren wir ein Rahmenwerk für abstrakte Interpretationen von Erlangprogrammen. Dieses Rahmenwerk garantiert, daß die abstrakte operationelle Semantik sicher bezüglich der Standardsemantik von Erlang ist. In diesem Zusammenhang bedeutet sicher, daß alle Pfade der Standardsemantik auch in der abstrakten operationellen Semantik enthalten sind. Wird dieses Rahmenwerk auf eine abstrakte Interpretation mit endlichem Wertebereich angewendet, so können viele Systemeigenschaften (wie z.B. Verklemmungsfreiheit, Lebendigkeit oder wechselseitiger Ausschluß) mittels Model Checking automatisch bewiesen werden. Da das Rahmenwerk eine sichere Abstraktion garantiert, gelten bewiesene Eigenschaften auch für die tatsächliche Ausführung des Erlangprogramms. In dieser Arbeit entwickeln wir das Rahmenwerk für Abstrakte Interpretationen von Erlang Programmen zur formalen Verifikation mittels Model Checking. Wir zeigen, wie das Rahmenwerk zum Model Checking für die Linearzeitlogik (Linear Time Logic) verwendet werden kann. Bei Erlangprogrammen mit nicht-endrekursiven Funktionsaufrufen, reicht die Datenabstraktion des Rahmenwerks nicht aus. Deshalb erweitern wir das Rahmenwerk um eine Abstraktion des Kontrollflusses. Alle präsentierten Techiken sind prototypisch in einem Verifikationstool implementiert. Wir zeigen die praktische Verwendbarkeit unseres Ansatzes und des Verifikationstools anhand der Verifikation eines Datenbankservers.

The functional programming language Erlang is successfully used for the development of distributed systems. We present an approach for the formal verification of Erlang programs using abstract interpretation and model checking. Therefore, we define a framework for abstract interpretations of Erlang programs. In this framework it is guaranteed that the abstract operational semantics is safe with respect to the standard semantics of Erlang. In this context, safe means that it contains all paths of the standard semantics. Applying this framework to a finite domain abstraction, many system properties (e.g. the absence of deadlocks and lifelocks or mutual exclusion) can automatically be proven by model checking. Since the framework guarantees safeness of the abstraction the properties proven for the abstraction also hold for the real execution of the Erlang program. In this theses, we develop the framework for abstract interpretations of Erlang programs for formal verification by model checking. We show how the framework can be used in model checking for Linear Time Logic. For Erlang programs containing non-tail recursive function calls data abstraction covered by our framework is not sufficient. Therefore, we extend the framework by abstraction of the control-flow. All presented techniques are prototypically implemented in a verification tool. We demonstrate the practical usability of our approach and the verification tool by the verification of a database server.

Fulltext:
PDF
(additional files)