论文标题
Quickstrom：具有LTL规格的基于属性的接受测试
Quickstrom: Property Based Acceptance Testing with LTL Specifications
论文作者
论文摘要
我们提出了QuickStrom，这是一种基于属性的测试系统，用于对交互式应用程序的接受测试。使用QuickStrom，程序员可以将Web应用程序的行为指定为我们称为QuickLTL的线性时间逻辑（LTL）的属性中的属性，然后自动在给定的规范的情况下自动测试其应用程序，并具有数百个自动生成的交互。 QuickLTL将LTL的现有有限变体用于测试用例，从而确定了最小长度本身由LTL公式决定的部分痕迹的结果。这种时间逻辑嵌入了我们的规范语言SpecStrom中，该语言旨在对Web程序员接近，表达了写作规格，并且易于分析。由于QuickStrom仅测试以用户的面向行为，因此对正在测试的系统的实现语言不可知。因此，我们正式指定并测试了流行的对Domvc基准测试的许多实现，该基准用于评估和比较各种Web前端框架和语言。我们的测试在几乎一半的可用实现中发现了错误。
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.
