ERCIM News No.32 - January 1998

Compositional Approach for Erlang Verification

by Mads Dam


The Formal Design Techniques Group at SICS has explored over the past few years a compositional approach to verification, in which verification goals are stated and proved in terms of the structure of programs. Such an approach makes it possible to state and prove properties of open systems.

With this approach, module encapsulation and proof reuse also become possible. Thus while an interactive, proof-based approach may introduce considerable overhead for small examples, by proving properties uniformly in model structure actual system configurations can be considered without size limits. The approach does not suffer from the problem of most theorem proving approaches, which is that reasoning takes place over explicit encodings, or representations, of programs and their semantics. Moreover it turns out that techniques such as model checking, even simulation and perhaps also testing, can be quite easily, and very tightly, embedded into a compositional approach, and vice versa. Much of our research program involves the fundamentals and applications of this compositional framework. Over the past months We have addressed these issues in the context of a prototype verifier being developed for the Erlang programming language in a collaboration with Ericsson. This work is likely to be central to our research for some time.

Verification of Erlang Programs

In the framework of a project between SICS and Ericsson Computer Science Laboratory, support will be provided for the verification (validation) of programs written in the Erlang programming language. Erlang, is an extremely high level symbolic functional programming language, developed at the Ericsson Computer Science Laboratory which is part of the research organisation of Ericsson. Erlang is similar to a scripting language, but unlike most scripting languages, it is efficient and extremely large modular systems can easily be designed . A large number of tools support system design using Erlang. Numerous libraries with reusable components are available.

So far verification addresses only a core fragment of the Erlang language. The means of verification is by utilising the theorem-prover tool, basically a proofchecker, but extended with considerable support for proof automation. The verification of an Erlang system typically involves the following steps:

In other words, programs are specified and verified in a modular way. Results obtained during the course of the project include:

For more information, see: http://www.sics.se/fdt/erlang.html

More information on Erlang can be found at: http://www.ericsson.se:800/cslab/erlang/

Please contact:

Mads Dam - SICS
Tel: +46 8 752 1549
E-mail: mfd@sics.se


return to the contents page