Abstract Blockchain implementations have become more and more advanced, combining many different features in the same framework (e.g., oracles, names, and state channels). Since the cost of errors in reputation and represented value is high in the blockchain world, software quality is of the utmost importance. One of the main methods used to assure such high software quality is careful testing. However, the number of tests needed to achieve a high level of assurance grows quadratic with the pairs of features of the blockchain, and when testing triples features the growth is cubic. To manually craft the required large number of tests is an almost impossible undertaking in practice. In this article, we describe how property‐based testing (PBT) techniques have been used to automate testing of the core part of the Aeternity blockchain, ensuring the high software quality of the blockchain. Even though PBT is a powerful testing technique, applying it to the task of testing a complex system such as a blockchain, is far from trivial. The structure of the Aeternity property‐based test model follows the structure of the blockchain, that is, it cleanly separates different blockchain features (e.g., oracles, smart contracts) into different model parts, and moreover, reduces the amount of boilerplate test model code by focusing on the identification of valid blockchain transactions. The test model is evaluated through a careful instrumentation of test code which permits observations of which combinations of features have been tested during a test run, and with which frequency. This article documents the details of how these issues were addressed in the development of the Aeternity test model, providing insights into both the testing of other blockchains as well as the testing of other complex feature based systems.

We address the problem of testing and debugging concurrent, distributed Erlang applications. In concurrent programs, race conditions are a common class of bugs and are very hard to find in practice. Traditional unit testing is normally unable to help finding all race conditions, because their occurrence depends so much on timing. Therefore, race conditions are often found during system testing, where due to the vast amount of code under test, it is often hard to diagnose the error resulting from race conditions. We present three tools (QuickCheck, PULSE, and a visualizer) that in combination can be used to test and debug concurrent programs in unit testing with a much better possibility of detecting race conditions. We evaluate our method on an industrial concurrent case study and illustrate how we find and analyze the race conditions.

We present a model checker for verifying distributed programs written in the Erlang programming language. Providing a model checker for Erlang is especially rewarding since the language is by now being seen as a very capable platform for developing industrial strength distributed applications with excellent failure tolerance characteristics. In contrast to most other Erlang verification attempts, we provide support for a very substantial part of the language. The model checker has full Erlang data type support, support for general process communication, node semantics (inter-process behave subtly different from intra-process communication), fault detection and fault tolerance through process linking, and can verify programs written using the OTP Erlang component library (used by most modern Erlang programs).