This article presents Makina, a library written in the Elixir programming language, and a domain specific language for writing property-based testing models for stateful programs. Models written in the domain specific language are translated into standard QuickCheck state machines. Our main goals with Makina are to facilitate the task of developing correct and maintainable models, and to encourage model reuse. To meet these goals, Makina provides a declarative syntax for defining model states and commands. In particular, Makina encourages the typing of specifications, and ensures that such type information can be used by Elixir type checking tools. Moreover, to promote model reuse, the domain specific language provides constructs that allow models to be defined in terms of collections of previously defined ones. To this end a number of operators for combining models have been defined and implemented in our library. A semantics for Makina models is presented in two steps. First, a novel operational semantics for standard QuickCheck state machine models is provided. Then, a translation from a Makina model to a standard QuickCheck state model is given.

This article provides a formal specification of the distribution and fault-tolerance mechanisms of eJason. The eJason programming language is an extension to the agent-oriented programming language Jason that introduces native support for the transparent distribution of agents as well as fault-tolerance mechanisms. This formal semantics is presented from a multiagent system perspective. It unambiguously describes both the possible evolution of the distributed multiagent system over time and the different instruments for fault detection and fault recovery, hence exposing their strengths. This specification may serve as a reference for researchers interested in the inclusion of similar mechanisms in agent-oriented programming languages. The formal semantics has been mechanized through an (open-source) implementation written in Prolog, which implements both the standard Jason operational semantics, along with the new rules for distribution and fault-tolerance introduced in this article.

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 present a framework for automatic grading of programming exercises using property-based testing, a form of model-based black-box testing. Models are developed to assess both the functional behaviour of programs and their algorithmic complexity. From the functional correctness model a large number of test cases are derived automatically. Executing them on the body of exercises gives rise to a (partial) ranking of programs, so that a program A is ranked higher than program B if it fails a strict subset of the test cases failed by B. The model for algorithmic complexity is used to compute worst-case complexity bounds. The framework moreover considers code structural metrics, such as McCabe's cyclomatic complexity, giving rise to a composite program grade that includes both functional, non-functional, and code structural aspects. The framework is evaluated in a course teaching algorithms and data structures using Java.

This article describes a systematic approach to testing behavioural aspects of Web Services that communicate using the JSON data format. As a key component, the Quviq QuickCheck property-based testing tool is used to automatically generate a large number of test cases from an abstract description of the service behaviour in the form of a finite state machine. The same behavioural description is also used to decide whether the execution of a test case is successful or not. To generate random JSON data for populating tests we have developed a new library, jsongen, which given a characterisation of the JSON data as a JSON schema, automatically derives a QuickCheck generator which is capable of generating an infinite number of JSON values that validate against the schema.