FMitF: Collaborative Research: User-Centered Verification and Repair of Trigger-Action Programs

现代以数据为中心的系统，从物联网设备到在线服务，都可以通过帮助人们明确他们的设备和服务应该如何行为以及彼此之间的交互而受益。通常，这需要人们参与一定数量的最终用户编程，或者由通常没有接受过编程培训的人进行编程。常见的例子包括指定只有当房间被占用时才应打开灯，或者指定主题行中包含特定单词的电子邮件应发送到特定文件夹。触发器-动作编程(TAP)由“如果-这-那么-那”规则组成，是终端用户编程最常见的模型，因为编写简单的TAP程序相对容易。然而，随着规则和设备的数量和复杂性的增加，TAP程序越来越多地受到错误和可靠性问题的困扰，对于缺乏经验和训练有素的程序员来说，很难纠正。该项目的目标是通过更好地了解最终用户的需求以及编写和调试TAP程序的能力，使TAP编程更强大，从而使人们与代表他们行事的设备交互的能力更加强大，开发出更好地模拟用户意图并建议满足用户意图的TAP程序的计算技术，以及使用这些技术帮助人们更容易创建正确的TAP程序的工具。除了对人民福祉的潜在好处外，该项目还将通过开发课程材料来提供教育好处，提高人们对方案编制的人的方面和正式方法的认识。此外，这种设备的有形性质和流行在线服务的熟悉性是吸引公众并在计算机科学研究生命周期中培训本科生、K-12学生和职业生涯早期研究生的一个肥沃领域。为了实现这些目标，这项工作结合了正规方法、人机交互和机器学习的技术。对形式化方法的贡献包括为终端用户编程环境中独特的程序修复、综合和规范细化问题设计系统的解决方案。对网络人类系统的贡献包括经验研究和设计数据驱动的界面，以更准确地表达意图。具体地说，经验性的人类受试者研究试图理解和改进触发动作编程的调试过程，创建和分发以用户为中心的触发动作程序集合的所需数据集，并比较评估所建议的接口。这项工作中开发的界面使用数据驱动的方法来帮助用户准确地定位和了解触发动作程序中的错误，以及在自动修复的触发动作程序的候选程序中进行选择。这些接口的底层将是触发-动作程序的正式模型，这些模型将根据在线性时态逻辑中编写的特定属性进行验证。开发的系统将系统地综合程序修复，考虑到用户的经验和偏好。该系统还将使用机器学习和正式方法的组合来自动生成触发动作程序，并根据用户与系统交互的历史痕迹总结规范。总而言之，通过触发式编程帮助非技术用户准确地传达他们的意图，有利于广泛部署的最终用户编程系统，用于集成互联网连接设备和在线服务。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Modern data-centric systems, ranging from Internet-of-Things devices to online services, can benefit from helping people make clear their intent for how their devices and services should behave and interact with each other. Generally, this requires people to engage in some amount of end-user programming, or programming by people who are not typically trained in programming. Common examples of this include specifying that a light should only turn on when a room is occupied or that emails with certain words in the subject line should be routed into a particular folder. Trigger-action programming (TAP), which consists of "if-this-then-that" rules, is the most common model for end-user programming because it is relatively easy to write simple TAP programs. However, as the number and complexity of both rules and devices increases, TAP programs increasingly suffer from bugs and dependability problems and are hard to correct for inexperienced and trained programmers alike. This project's goal is to make TAP programming, and thus people's ability to interact with devices that act on their behalf, more robust through developing a better understanding of end users' needs and abilities to write and debug TAP programs, computational techniques to both better model user intents and suggest TAP programs that meet them, and tools that use those techniques to help people more easily create correct TAP programs. Apart from the potential benefits to people's well-being, the project will also provide educational benefits by developing course materials that increase awareness of both human aspects of, and formal methods for, programming. Further, the tangible nature of such devices and the familiarity of popular online services are a fertile domain for engaging the public and training undergraduate students, K-12 students, and early-career graduate students in the computer science research lifecycle.To accomplish these goals, the work combines techniques from formal methods, human-computer interaction, and machine learning. Contributions to formal methods include the design of systematic solutions to unique program repair, synthesis, and specification-refinement problems in the context of end-user programming. Contributions to cyber human systems include empirical studies and the design of data-driven interfaces for more accurately expressing intent. Specifically, the empirical human subjects studies seek to understand and improve the debugging process for trigger-action programming, create and distribute needed data sets of user-centric collections of trigger-action programs, and comparatively evaluate proposed interfaces. The interfaces developed in this work use data-driven methods to help users pinpoint and understand bugs in trigger-action programs, as well as to choose among candidates for automatically repaired trigger-action programs. Underlying these interfaces will be formal models of trigger-action programs, which are verified against specified properties written in linear temporal logic. The system developed will systematically synthesize program repairs, taking into account users' experiences and preferences. The system will also use a combination of machine learning and formal methods to automatically generate trigger-action programs and summarize specifications based on historical traces of user interaction with the system. In sum, helping non-technical users accurately communicate their intent through trigger-action programming benefits widely deployed end-user-programming systems for integrating internet-connected devices and online services.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.