Quickstrom：基于性能的验收测试，符合LTL规范
Quickstrom: Property Based Acceptance Testing with LTL Specifications
摘要：
我们提出了Quickstrom，一个基于属性的测试系统，用于交互式应用程序的验收测试。使用Quickstrom，程序员可以将Web应用程序的行为指定为我们称为QuickLTL的面向测试的线性时序逻辑（LTL）方言中的属性，然后根据给定的规范自动测试他们的应用程序，并自动生成数百个交互。QuickLTL为测试用例扩展了LTL的现有有限变体，确定了部分跟踪的可能结果，这些跟踪的最小长度本身由LTL公式确定。这种时态逻辑嵌入在我们的规约语言Specstrom中，它被设计成Web程序员可以访问的，用于编写规范的表达，并且易于分析。因为Quickstrom只测试面向用户的行为，所以它与被测系统的实现语言无关。因此，我们正式指定并测试了流行的TodoMVC基准的许多实现，用于在各种Web前端框架和语言之间进行评估和比较。我们的测试在几乎一半的可用实现中发现了bug。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
