Property-Based Testing for Asynchronous Functional Reactive Programming Using Linear Temporal Logic

Abstract

Functional reactive programming (FRP) is a programming paradigm for implementing software that continuously interacts with its environment and manipulates highly dynamic data. Asynchronous FRP, in particular, is very expressive and can be used to implement graphical user interfaces and other reactive systems interacting with data streams and events that are not synchronized. Testing such asynchronous FRP programs is difficult since a program's behaviour depends not only on the concrete data it receives from its environment but also the relative timing of when each piece of data arrives.

In this paper, we propose PropRatt, a property-based testing framework for asynchronous FRP. The key component of PropRatt is its specification language, which extends basic linear temporal logic with a means to express properties of several concurrent signals. This allows us to express temporal properties that relate data coming from different signals at different points in time. PropRatt is implemented in Haskell and targets a recently introduced asynchronous FRP language embedded in Haskell. We demonstrate the utility of PropRatt through a case study testing a signal combinator library as well as a graphical user interface, in which we suggest how the strategy for generating signals can be modified to better model specific domains.

Keywords: Property-based Testing, Functional Reactive Programming Linear Temporal Logic