SHF:Small:Proving User Interface Testing Programs Correct

图形用户界面（GUI）在当今的计算世界中无处不在，它消耗了GUI应用程序（GAP）软件开发成本的60%，以及代码的45-60%。对于一个越来越依赖gap来管理用户生活各个方面的社会来说，确保gap的质量是极其重要的。目前，虽然有数百种GUI测试方法、算法和工具，但该领域非常分散，缺乏共同的抽象，并且很难整合不同的UI测试方法，从而创建强大的解决方案来解决重用和修复UI测试套件的问题，同时减少其执行时间和资源需求（R3）。因此，本提案的目标是创建一个新的理论基础，将这些R3问题与证明复杂用户界面测试程序（PUITs）行为的问题联系起来，特别是当GAP的结构和功能在其演变和维护过程中不断变化时。本提案的研究重点中的一个连接线是使用Eilenberg的X-Machine将puit抽象为功能反应系统，这是有限状态自动机（FSA）的概括，其中状态转换与在FSA数据上操作的函数相关。测试工程师将使用称为Coq的证明管理系统中的正式函数语言创建puit。研究小组正在扩展Coq的Razet定理包，其中包含对Eilenberg的X-Machine的一般证明，使用从GAP FSA生成的类型应用于任意GAP。由于GAP的物理结构是从其puit中抽象出来的，因此可以看到它们的重用将在不同的功能相关的GAP上启用。结果验证的可执行puit可以使用Coq的生成工具以目标语言自动生成。所提出的研究方向的好处远远大于其组成部分的总和，因为出现了一种面向类型验证的新属性，它可以使用UI对象中的数据语义创建puit的自动推理，并且使测试工程师不仅可以证明puit的正确性，还可以从统一的角度解决R3问题。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

The Graphical User Interface (GUI) that is ubiquitous in today's computing world consumes about 60% of the software development cost of a GUI APplication (GAP) and as much as 45-60% of its code. Ensuring the quality of GAPs is extremely important for a society that is increasingly reliant on GAPs to manage all aspects of users' lives. Currently, although there are hundreds of GUI testing approaches, algorithms and tools, the field is deeply fragmented and lacks common abstractions, and it is very difficult to integrate different UI testing approaches so as to create powerful solutions to the problems of Reusing and Repairing UI test suites while also Reducing their execution time and resource demands (R3). The goal of this proposal is therefore to create a novel theoretical foundation to connect these R3 problems with the problem of proving the behavior of complex Programs for User Interface Testing (PUITs), especially when the structure and the functionality of a GAP is constantly changed during its evolution and maintenance. A connecting thread in the research thrusts of this proposal is to abstract PUITs as functional reactive systems using Eilenberg's X-Machine, which is a generalization of a Finite State Automaton (FSA) in which state transitions are associated with functions which operate on the FSA's data. Test engineers are to create PUITs using a formal functional language in a proof management system called Coq. The research team is expanding the Razet theorem package for Coq that contains a generic proof for Eilenberg's X-Machine to apply to arbitrary GAPs using the types generated from the GAP FSA. Since the physical structure of the GAP is abstracted away from its PUITs, it is being shown that their reuse will be enabled on different functionally related GAPs. The resulting verified executable PUITs can be generated automatically in a target language using the Coq's generation facilities. The benefits of the proposed research direction are much bigger than the sum of its constituent parts since a new property of type-directed verification emerges that enables automated reasoning of PUITs, which are created using the semantics of the data in the UI objects, and that enable test engineers not only to prove PUITs correct but also to address R3 problems from a unified perspective.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.