|

Model checking Erlang code

Research by

Summary

Verification of Erlang code via model checking a process algebraic abstraction.

Why and how?

My PhD student Clara Benac Earle has been investigating the application of formal methods for the verification of software. In particular she has written an algorithm for resource management (we refer to it as the locker) which is inspired in a critical part of the control software of the AXD 301 ATM switch built by Ericsson. This software is written in the functional programming language Erlang. She, in collaboration with others (in particular Thomas Arts), have built a tool that translates the Erlang code into a process algebra specification (µCRL, LOTOS). To specify properties that should hold in the program, an alternation-free variant of µ-Calculus is used, and several properties have been checked with the Caesar/Aldebaran model checker.