From Temporal Models to Property-Based Testing

TL;DR

This paper introduces a framework that translates temporal formal models into executable Scala code using BeSpaceD, enabling property-based testing to improve understanding and verification of temporal system properties.

Contribution

It presents a novel approach to apply property-based testing directly on formal temporal models by translating them into executable code, bridging formal methods and testing.

Findings

Framework successfully translates TLA+ and FocusST models into Scala code.

Enables property-based testing of formal temporal models.

Improves understanding and verification of temporal properties.

Abstract

This paper presents a framework to apply property-based testing (PBT) on top of temporal formal models. The aim of this work is to help software engineers to understand temporal models that are presented formally and to make use of the advantages of formal methods: the core time-based constructs of a formal method are schematically translated to the BeSpaceD extension of the Scala programming language. This allows us to have an executable Scala code that corresponds to the formal model, as well as to perform PBT of the models functionality. To model temporal properties of the systems, in the current work we focus on two formal languages, TLA+ and FocusST.