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

FMITF：协作研究：以用户为中心的触发操作程序验证和修复

• 批准号: 1837120
• 负责人: Blase Ur
• 金额: $ 66.67万
• 依托单位: University of Chicago
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2018
• 资助国家: 美国
• 起止时间: 2018-09-01 至 2022-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1837120&HistoricalAwards=false
• 关键词: FMitF; Collaborative; Research; User; Centered

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.

以数据为中心的系统，从物联网设备到在线服务，可以帮助人们明确意图对他们的设备和服务应如何行事和互动。 通常，这要求人们进行一定数量的最终用户编程或通常不受编程培训的人进行编程。 其中的常见示例包括指定只有在房间被占用时才能打开灯，或者应将主题行中的某些单词的电子邮件路由到特定文件夹中。 由“如果这样的”规则组成的Trigger-Action编程（TAP）是最终用户编程的最常见模型，因为它相对容易编写简单的TAP程序。 但是，随着规则和设备的数量和复杂性的增加，TAP程序越来越遭受错误和可靠性问题的困扰，并且很难纠正经验不足和训练有素的程序员。 该项目的目标是制作敲击编程，因此人们与代表他们行动的设备进行互动，通过更好地了解最终用户的需求和能力来编写和调试的能力，从而更强大，计算技术，以更好地模型用户的意图，并建议使用这些技术来帮助人们更轻松地创建Paps Paps程序。 除了对人们的福祉带来的潜在利益外，该项目还将通过开发课程材料来提高对编程的人类方面和正式方法的认识，从而提供教育益处。 此外，此类设备的切实本质以及流行的在线服务的熟悉程度是一个肥沃的领域，可以吸引公众和培训本科生，K-12学生和计算机科学研究生命周期的早期研究生研究生。为了实现这些目标，该工作结合了从形式上的技术来实现技术，人类计算机的互动和机器学习。对正式方法的贡献包括在最终用户编程的背景下设计系统解决方案，以设计独特的程序修复，合成和规范 - 进行限制问题。对网络人类系统的贡献包括实证研究和数据驱动界面的设计，以更准确地表达意图。具体而言，经验的人类主题研究试图了解和改善触发器编程，创建和分发以用户为中心的触发程序程序集合的数据集以及相对评估所提出的接口的调试过程。在这项工作中开发的接口使用数据驱动的方法来帮助用户查明和了解触发程序程序中的错误，以及在候选人中选择自动修复的触发动作程序。这些接口的基础将是触发进程程序的正式模型，这些模型可根据线性时间逻辑编写的指定属性进行验证。开发的系统将在考虑用户的经验和偏好方面系统地综合程序维修。该系统还将使用机器学习和形式方法的组合来自动生成触发程序程序，并根据用户与系统交互的历史痕迹总结规范。总而言之，通过触发作用编程好处，可以帮助非技术用户准确地传达其意图，以整合Internet连接设备和在线服务，广泛部署的最终用户程序编程系统。该奖项反映了NSF的法定任务，并被认为是通过基金会的知识分子的知识和更广泛的影响来通过评估来评估的，并认为值得一提。

项目成果

AutoTap: Synthesizing and Repairing Trigger-Action Programs Using LTL Properties

• DOI: 10.1109/icse.2019.00043
• 发表时间: 2019-01-01
• 期刊: 2019 IEEE/ACM 41ST INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE 2019)
• 作者: Zhang, Lefan;He, Weijia;Ur, Blase
• 通讯作者: Ur, Blase

Understanding Trigger-Action Programs Through Novel Visualizations of Program Differences

• DOI: 10.1145/3411764.3445567
• 发表时间: 2021-05
• 期刊: Proceedings of the 2021 CHI Conference on Human Factors in Computing Systems
• 作者: Valerie Zhao;Lefan Zhang;Bo Wang;M. Littman;Shan Lu;Blase Ur

Helping Users Debug Trigger-Action Programs

• DOI: 10.1145/3569506
• 发表时间: 2022-12
• 期刊: Proceedings of the ACM on Interactive, Mobile, Wearable and Ubiquitous Technologies
• 作者: Lefan Zhang;Cyrus Zhou;M. Littman;Blase Ur;Shan Lu

Supporting End Users in Defining Reinforcement-Learning Problems for Human-Robot Interactions (Extended Abstract)

支持最终用户定义人机交互的强化学习问题（扩展摘要）

• 发表时间: 2022
• 期刊: The 5th Multidisciplinary Conference on Reinforcement Learning and Decision Making (RLDM
• 作者: Zhao, Valerie;Littman, Michael L.;Lu, Shan;Sebo, Sarah;Ur, Blase
• 通讯作者: Ur, Blase

When Smart Devices Are Stupid: Negative Experiences Using Home Smart Devices

• DOI: 10.1109/spw.2019.00036
• 发表时间: 2019-01-01
• 期刊: 2019 IEEE Security and Privacy Workshops (SPW). Proceedings
• 作者: Weijia He;Martinez, Jesse;Ur, Blase
• 通讯作者: Ur, Blase