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

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

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.