Runtime verification in Erlang by using contracts

TL;DR

This paper introduces a contract-based runtime verification system for Erlang, enabling error detection during execution and supporting both general and concurrent program contracts, with implementation details and open-source code.

Contribution

It presents the design and implementation of EDBC, a novel runtime verification system for Erlang using design-by-contract principles, including support for concurrent programs.

Findings

Implemented two types of contracts for Erlang

Provided detailed examples and explanations

Made the system available as open-source on GitHub

Abstract

During its lifetime, a program suffers several changes that seek to improve or to augment some parts of its functionality. However, these modifications usually also introduce errors that affect the already-working code. There are several approaches and tools that help to spot and find the source of these errors. However, most of these errors could be avoided beforehand by using some of the knowledge that the programmers had when they were writing the code. This is the idea behind the design-by-contract approach, where users can define contracts that can be checked during runtime. In this paper, we apply the principles of this approach to Erlang, enabling, in this way, a runtime verification system in this language. We define two types of contracts. One of them can be used in any Erlang program, while the second type is intended to be used only in concurrent programs. We provide the details of the implementation of both types of contracts. Moreover, we provide an extensive explanation of each contract as well as examples of their usage. All the ideas presented in this paper have been implemented in a contract-based runtime verification system named EDBC. Its source code is available at GitHub as an open-source and free project.