Quickstrom: property-based acceptance testing with LTL specifications

Liam O'Connor; Oskar Wickström

doi:10.48550/arXiv.2203.11532

Quickstrom: property-based acceptance testing with LTL specifications

Liam O'Connor, Oskar Wickström

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

We present Quickstrom, a property-based testing system for acceptance testing of interactive applications. Using Quickstrom, programmers can specify the behaviour of web applications as properties in our testing-oriented dialect of Linear Temporal Logic (LTL) called QuickLTL, and then automatically test their application against the given specification with hundreds of automatically generated interactions. QuickLTL extends existing finite variants of LTL for the testing use-case, determining likely outcomes from partial traces whose minimum length is itself determined by the LTL formula. This temporal logic is embedded in our specification language, Specstrom, which is designed to be approachable to web programmers, expressive for writing specifications, and easy to analyse. Because Quickstrom tests only user-facing behaviour, it is agnostic to the implementation language of the system under test. We therefore formally specify and test many implementations of the popular TodoMVC benchmark, used for evaluation and comparison across various web frontend frameworks and languages. Our tests uncovered bugs in almost half of the available implementations.

Original language	English
Title of host publication	Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation
Editors	Ranjit Jhala, Işil Dillig
Place of Publication	New York, NY, USA
Publisher	ACM Association for Computing Machinery
Pages	1025-1038
Number of pages	14
ISBN (Electronic)	978-1-4503-9265-5
DOIs	https://doi.org/10.48550/arXiv.2203.11532 https://doi.org/10.1145/3519939.3523728
Publication status	Published - 9 Jun 2022
Event	43rd ACM SIGPLAN Conference on Programming Language Design and Implementation - San Diego, United States Duration: 15 Jun 2022 → 17 Jun 2022 Conference number: 43 https://pldi22.sigplan.org/

Conference

Conference	43rd ACM SIGPLAN Conference on Programming Language Design and Implementation
Abbreviated title	PLDI 2022
Country/Territory	United States
City	San Diego
Period	15/06/22 → 17/06/22
Internet address	https://pldi22.sigplan.org/

Keywords / Materials (for Non-textual outputs)

property-based testing
linear temporal logic
web fronted programming
semantics

Access to Document

10.48550/arXiv.2203.11532Licence: Creative Commons: Attribution-ShareAlike (CC-BY-SA)
10.1145/3519939.3523728Licence: All Rights Reserved

Quickstrom_OCONNOR_DOA25022022_AFVAccepted author manuscript, 724 KBLicence: Creative Commons: Attribution (CC-BY)

https://dl.acm.org/doi/10.1145/3519939.3523728Licence: All Rights Reserved

Cite this

O'Connor, L., & Wickström, O. (2022). Quickstrom: property-based acceptance testing with LTL specifications. In R. Jhala, & I. Dillig (Eds.), Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (pp. 1025-1038). ACM Association for Computing Machinery. https://doi.org/10.48550/arXiv.2203.11532, https://doi.org/10.1145/3519939.3523728

@inproceedings{709675d1166149a6aa4756d48143083f,

title = "Quickstrom: property-based acceptance testing with LTL specifications",

abstract = "We present Quickstrom, a property-based testing system for acceptance testing of interactive applications. Using Quickstrom, programmers can specify the behaviour of web applications as properties in our testing-oriented dialect of Linear Temporal Logic (LTL) called QuickLTL, and then automatically test their application against the given specification with hundreds of automatically generated interactions. QuickLTL extends existing finite variants of LTL for the testing use-case, determining likely outcomes from partial traces whose minimum length is itself determined by the LTL formula. This temporal logic is embedded in our specification language, Specstrom, which is designed to be approachable to web programmers, expressive for writing specifications, and easy to analyse. Because Quickstrom tests only user-facing behaviour, it is agnostic to the implementation language of the system under test. We therefore formally specify and test many implementations of the popular TodoMVC benchmark, used for evaluation and comparison across various web frontend frameworks and languages. Our tests uncovered bugs in almost half of the available implementations.",

keywords = "property-based testing, linear temporal logic, web fronted programming, semantics",

author = "Liam O'Connor and Oskar Wickstr{\"o}m",

note = "Publisher Copyright: {\textcopyright} 2022 ACM.; 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2022 ; Conference date: 15-06-2022 Through 17-06-2022",

year = "2022",

month = jun,

day = "9",

doi = "10.48550/arXiv.2203.11532",

language = "English",

pages = "1025--1038",

editor = "Ranjit Jhala and I{\c s}il Dillig",

booktitle = "Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation",

publisher = "ACM Association for Computing Machinery",

url = "https://pldi22.sigplan.org/",

}

O'Connor, L & Wickström, O 2022, Quickstrom: property-based acceptance testing with LTL specifications. in R Jhala & I Dillig (eds), Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. ACM Association for Computing Machinery, New York, NY, USA, pp. 1025-1038, 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation, San Diego, California, United States, 15/06/22. https://doi.org/10.48550/arXiv.2203.11532, https://doi.org/10.1145/3519939.3523728

Quickstrom: property-based acceptance testing with LTL specifications. / O'Connor, Liam; Wickström, Oskar.
Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. ed. / Ranjit Jhala; Işil Dillig. New York, NY, USA: ACM Association for Computing Machinery, 2022. p. 1025-1038.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Quickstrom: property-based acceptance testing with LTL specifications

AU - O'Connor, Liam

AU - Wickström, Oskar

N1 - Conference code: 43

PY - 2022/6/9

Y1 - 2022/6/9

N2 - We present Quickstrom, a property-based testing system for acceptance testing of interactive applications. Using Quickstrom, programmers can specify the behaviour of web applications as properties in our testing-oriented dialect of Linear Temporal Logic (LTL) called QuickLTL, and then automatically test their application against the given specification with hundreds of automatically generated interactions. QuickLTL extends existing finite variants of LTL for the testing use-case, determining likely outcomes from partial traces whose minimum length is itself determined by the LTL formula. This temporal logic is embedded in our specification language, Specstrom, which is designed to be approachable to web programmers, expressive for writing specifications, and easy to analyse. Because Quickstrom tests only user-facing behaviour, it is agnostic to the implementation language of the system under test. We therefore formally specify and test many implementations of the popular TodoMVC benchmark, used for evaluation and comparison across various web frontend frameworks and languages. Our tests uncovered bugs in almost half of the available implementations.

AB - We present Quickstrom, a property-based testing system for acceptance testing of interactive applications. Using Quickstrom, programmers can specify the behaviour of web applications as properties in our testing-oriented dialect of Linear Temporal Logic (LTL) called QuickLTL, and then automatically test their application against the given specification with hundreds of automatically generated interactions. QuickLTL extends existing finite variants of LTL for the testing use-case, determining likely outcomes from partial traces whose minimum length is itself determined by the LTL formula. This temporal logic is embedded in our specification language, Specstrom, which is designed to be approachable to web programmers, expressive for writing specifications, and easy to analyse. Because Quickstrom tests only user-facing behaviour, it is agnostic to the implementation language of the system under test. We therefore formally specify and test many implementations of the popular TodoMVC benchmark, used for evaluation and comparison across various web frontend frameworks and languages. Our tests uncovered bugs in almost half of the available implementations.

KW - property-based testing

KW - linear temporal logic

KW - web fronted programming

KW - semantics

U2 - 10.48550/arXiv.2203.11532

DO - 10.48550/arXiv.2203.11532

M3 - Conference contribution

SP - 1025

EP - 1038

BT - Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation

A2 - Jhala, Ranjit

A2 - Dillig, Işil

PB - ACM Association for Computing Machinery

CY - New York, NY, USA

T2 - 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation

Y2 - 15 June 2022 through 17 June 2022

ER -

O'Connor L, Wickström O. Quickstrom: property-based acceptance testing with LTL specifications. In Jhala R, Dillig I, editors, Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. New York, NY, USA: ACM Association for Computing Machinery. 2022. p. 1025-1038 doi: 10.48550/arXiv.2203.11532, 10.1145/3519939.3523728

Quickstrom: property-based acceptance testing with LTL specifications

Abstract

Conference

Keywords / Materials (for Non-textual outputs)

Access to Document

Fingerprint

Cite this