CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

McErlang: A Model Checker for a Distributed Functional Programming Language

Lars-Åke Fredlund ; Hans Svensson (Institutionen för data- och informationsteknik, Datavetenskap (Chalmers))
Proc. of International Conference on Functional Programming (ICFP) p. 125-136. (2007)
[Konferensbidrag, refereegranskat]

We present a model checker for verifying distributed programs written in the Erlang programming language. Providing a model checker for Erlang is especially rewarding since the language is by now being seen as a very capable platform for developing industrial strength distributed applications with excellent failure tolerance characteristics. In contrast to most other Erlang verification attempts, we provide support for a very substantial part of the language. The model checker has full Erlang data type support, support for general process communication, node semantics (inter-process behave subtly different from intra-process communication), fault detection and fault tolerance through process linking, and can verify programs written using the OTP Erlang component library (used by most modern Erlang programs). As the model checking tool is itself implemented in Erlang we benefit from the advantages that a (dynamically typed) functional programming language offers: easy prototyping and experimentation with new verification algorithms, rich executable models that use complex data structures directly programmed in Erlang, the ability to treat executable models interchangeably as programs (to be executed directly by the Erlang interpreter) and data, and not least the possibility to cleanly structure and to cleanly combine various verification sub-tasks. In the paper we discuss the design of the tool and provide early indications on its performance.



Denna post skapades 2007-10-08.
CPL Pubid: 52081

 

Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Datavetenskap (Chalmers)

Ämnesområden

Programvaruteknik

Chalmers infrastruktur

Relaterade publikationer

Denna publikation ingår i:


Verification of Distributed Erlang Programs using Testing, Model Checking and Theorem Proving