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