Verification of Erlang programs using abstract interpretation and model checking

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.

Grantor dc:publisher

Publikationsserver der RWTH Aachen University

Year dc:date

2001

Author dc:creator

• Huch, Frank Günter

Contributors dc:contributor

• Indermark, Klaus

• info:eu-repo/classification/ddc/004
• Informatik
• Verteiltes System
• Softwareentwicklung
• Funktionale Programmiersprache
• Programmverifikation
• Model checking
• Abstrakte Interpretation
• Erlang
• Verification
• Abstraction

Statement dc:rights

• info:eu-repo/semantics/openAccess

Language dc:language

eng

Identifier

https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-121207%22

OAI identifier oai:identifier

oai:publications.rwth-aachen.de:59420