COPLAS Talk: Liam O'Connor, Quickstrom: Property-based Acceptance Testing with LTL Specifications

Speaker

Liam O'Connor specialises in the intersection of programming languages and formal methods research. He is a Lecturer in Programming Languages for Trustworthy Systems at the University of Edinburgh. For seven years he worked with the Trustworthy Systems group at UNSW in Australia, on projects such as the verified microkernel seL4,  and the development of certifying compilers for the development of trustworthy file systems. Liam has also published in the area of dependently-typed programming and proving, and has other interests ranging from concurrency to software engineering. Lately, his focus has been on bringing the techniques for specification and verification developed in the formal methods community into programming languages and software engineering tools.

Title

Quickstrom: Property-based Acceptance Testing with LTL Specifications

Abstract

Tools like Selenium WebDriver enable automated acceptance testing of user interfaces for web applications, and have seen widespread adoption. Unfortunately, programmers must painstakingly specify individual test cases themselves, which hearkens back to the dark ages of unit tests before property-based testing. Quickstrom aims to bring the magic of property-based testing to this domain. 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.

Host

Fritz Henglein (DIKU)

All are welcome. No registration required.  Feel free to forward this invitation. 

The Copenhagen Programming Languages Seminar (COPLAS) is a collaboration between DTU, ITU, Roskilde University and UCPH. To be informed about COPLAS activities and related talks, join this mailing list.