System Description: Verification of Distributed Erlang Programs

Introduction Software written for telecommunication applications has to meet high quality demands. Correctness is one major concern; the activity of proving formally that a system is correct is called verification. Telecommunications software is highly concurrent, and testing is often not capable of guaranteeing correctness to a satisfactory degree. The software we are faced with consists of many, relatively small modules, written in the functional language Erlang [AVWW96]. These modules define the behaviour of a number of processes operating in parallel and communicating through asynchronous message-passing. New processes can be generated during execution. Because of the complexity of such software, our approach to verification is to prove that the software satisfies a set of properties formally specified in a suitable logic language. The specification language we use is based on Park's ¯-calculus [Par76,Koz83]