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:
- formulating the desired behaviour of the Erlang system in a specification
logic
- describing the relevant behaviour of the component processes of the
system in the same logic
- prove that the components satisfy their specifications using the theorem
prover
- prove that when a system is constructed using components that satisfy
the component specifications, then such a system will satisfy the system
correctness criterium formulated in step 1 above.
In other words, programs are specified and verified in a modular way.
Results obtained during the course of the project include:
- operational semantics for variations of Erlang, eg, for interleaving
and sequential evaluation orders
- a specification logic (based on the mu-calculus) for formulating the
essential behaviour of Erlang programs precisely and compactly
- a proof system for inferring whether an Erlang program (a collection
of processes) satisfies a property described in the specification logic;
in contrast to many other such proof systems our approach handles dynamic
creation of new (Erlang) processes during the execution of the analysed
program
- proof-checking tool with support for automation of common tasks.
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
