SHF:Small:Proving User Interface Testing Programs Correct

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

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.