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

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

• 批准号: 1836948
• 负责人: George Konidaris
• 金额: $ 33.33万
• 依托单位: Brown University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2018
• 资助国家: 美国
• 起止时间: 2018-09-01 至 2022-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1836948&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.

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

项目成果

On the Expressivity of Markov Reward

• 发表时间: 2021-11
• 期刊: ArXiv
• 作者: David Abel;Will Dabney;A. Harutyunyan;Mark K. Ho;M. Littman;Doina Precup;Satinder Singh

Stackelberg Punishment and Bully-Proofing Autonomous Vehicles

Stackelberg 惩罚和防欺凌自动驾驶汽车

• DOI: 10.1007/978-3-030-35888-4_34
• 发表时间: 2019
• 期刊: ICSR 2019: Social Robotics
• 作者: Cooper, Matt;Lee, Jun Ki;Beck, Jacob;Fishman, Joshua D.;Gillett, Michael;Papakipos, Zoe;Zhang, Aaron;Ramos, Jerome;Shah, Aansh;Littman, Michael L.
• 通讯作者: Littman, Michael L.

Applying prerequisite structure inference to adaptive testing

• DOI: 10.1145/3375462.3375541
• 发表时间: 2020-03
• 期刊: Proceedings of the Tenth International Conference on Learning Analytics & Knowledge
• 作者: S. Saarinen;Evan Cater;M. Littman

Teaching a Robot Tasks of Arbitrary Complexity via Human Feedback

通过人类反馈教机器人执行任意复杂的任务

• DOI: 10.1145/3319502.3374824
• 发表时间: 2020
• 期刊: Human Robot Interaction (HRI'20
• 作者: Wang, Guan;Trimbach, Carl;Lee, Jun Ki;Ho, Mark K.;Littman, Michael L.
• 通讯作者: Littman, Michael L.

Evidence Humans Provide When Explaining Data-Labeling Decisions

• DOI: 10.1007/978-3-030-29387-1_22
• 发表时间: 2019-09
• 期刊: ArXiv
• 作者: J. Newman;Bo Wang;Valerie Zhao;Amy Zeng;M. Littman;Blase Ur