Runtime verification in Erlang by using contracts

[EN] During its lifetime, a program regularly undergoes changes that seek to improve its functionality or efficiency. However, such modifications may also introduce new errors. In this work, we use the designby-contract approach to allow programmers to formally state, in the code, some of the knowledge and assumptions originally made when the code was first written. Such contracts can then be checked at runtime, to ensure that modifications made to a program did not violate those assumptions. Applying these principles we have designed a runtime verification system for the Erlang language, permitting to specify as annotations the contracts needed for both sequential and concurrent code. As a second contribution we extend the commonly used Erlang gen server behaviour (a design pattern) permitting to specify declaratively when a server is ready to service a client request. The ideas presented in this paper have been implemented in a tool named EDBC. Its source code is available at github.com as an open-source and free project.