CPS: Synergy: Collaborative Research: Autonomy Protocols: From Human Behavioral Modeling to Correct-By-Construction, Scalable Control

CPS：协同：协作研究：自主协议：从人类行为建模到构建纠正、可扩展控制

• 批准号: 1446578
• 负责人: Behcet Acikmese
• 金额: $ 64.85万
• 依托单位: University of Texas at Austin
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2014
• 资助国家: 美国
• 起止时间: 2014-10-01 至 2016-03-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1446578&HistoricalAwards=false
• 关键词: CPS; Synergy; Collaborative; Research; Autonomy

Computer systems are increasingly coming to be relied upon to augment or replace human operators in controlling mechanical devices in contexts such as transportation systems, chemical plants, and medical devices, where safety and correctness are critical. A central problem is how to verify that such partially automated or fully autonomous cyber-physical systems (CPS) are worthy of our trust. One promising approach involves synthesis of the computer implementation codes from formal specifications, by software tools. This project contributes to this "correct-by-construction" approach, by developing scalable, automated methods for the synthesis of control protocols with provable correctness guarantees, based on insights from models of human behavior. It targets: (i) the gap between the capabilities of today's hardly autonomous, unmanned systems and the levels of capability at which they can make an impact on our use of monetary, labor, and time resources; and (ii) the lack of computational, automated, scalable tools suitable for the specification, synthesis and verification of such autonomous systems.The research is based on study of modular reinforcement learning-based models of human behavior derived through experiments designed to elicit information on how humans control complex interactive systems in dynamic environments, including automobile driving. Architectural insights and stochastic models from this study are incorporated with a specification language based on linear temporal logic, to guide the synthesis of adaptive autonomous controllers. Motion planning and other dynamic decision-making are by algorithms based on computational engines that represent the underlying physics, with provision for run-time adaptation to account for changing operational and environmental conditions. Tools implementing this methodology are validated through experimentation in a virtual testing facility in the context of autonomous driving in urban environments and multi-vehicle autonomous navigation of micro-air vehicles in dynamic environments. Education and outreach activities include involvement of undergraduate and graduate students in the research, integration of the research into courses, demonstrations for K-12 students, and recruitment of research participants from under-represented demographic groups. Data, code, and teaching materials developed by the project are disseminated publicly on the Web.

在交通系统、化工厂和医疗设备等安全性和正确性至关重要的环境中，越来越多地依赖计算机系统来增强或取代人类操作员控制机械设备。一个核心问题是如何验证这种部分自动化或完全自主的网络物理系统（CPS）是否值得我们信任。一种有前途的方法涉及通过软件工具根据正式规范合成计算机实现代码。该项目基于人类行为模型的见解，开发可扩展的自动化方法来合成具有可证明正确性保证的控制协议，从而为这种“构建正确”方法做出了贡献。它的目标是：（i）当今难以自主的无人系统的能力与它们对我们对货币、劳动力和时间资源的使用产生影响的能力水平之间的差距； (ii) 缺乏适合此类自主系统的规范、综合和验证的计算、自动化、可扩展工具。该研究基于对基于模块化强化学习的人类行为模型的研究，这些模型是通过实验得出的，旨在获取有关人类如何在动态环境（包括汽车驾驶）中控制复杂交互系统的信息。这项研究的架构见解和随机模型与基于线性时序逻辑的规范语言相结合，以指导自适应自主控制器的综合。运动规划和其他动态决策是通过基于代表底层物理的计算引擎的算法进行的，并提供运行时适应以适应不断变化的操作和环境条件。实现该方法的工具通过在城市环境中的自动驾驶和动态环境中的微型飞行器的多车辆自主导航的背景下在虚拟测试设施中进行的实验进行验证。教育和推广活动包括本科生和研究生参与研究、将研究纳入课程、为 K-12 学生进行演示，以及从代表性不足的人口群体中招募研究参与者。该项目开发的数据、代码和教材在网络上公开传播。