权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

InTrans: TRI-MIT Collaboration on Formal Verification Meets Big Data Intelligence in the Trillion Miles Challenge

InTrans：TRI-MIT 形式验证合作在万亿英里挑战中迎接大数据智能

基本信息

批准号：
1665282
负责人：
Armando Solar-Lezama
金额：
$ 23.2万
依托单位：
Massachusetts Institute of Technology
依托单位国家：
美国
项目类别：
Continuing Grant
财政年份：
2017
资助国家：
美国
起止时间：
2017-03-01 至 2019-02-28
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=1665282&HistoricalAwards=false
关键词：
InTrans TRI MIT Collaboration Formal

项目摘要

The goal of this project is to leverage the Synthesis and automated reasoning techniques developed as part of the project titled "Expeditions in Computer Aided Program Engineering (ExCAPE): Harnessing Synthesis for Software Design" in order to help ensure the safety of self driving vehicles. Self-driving vehicles involve a combination of perception, planning, control and algorithms that are too complex to be fully verified to guarantee complete reliability, but the goal is to show that individual components can be verified to work correctly under many important scenarios. One of the key innovations in this project is to show that synthesis technology has a role to play in this challenging task. Synthesis generally aims at generating a piece of code whose behavior satisfies some constraints, but the ExCAPE project demonstrated an important application of synthesis: generating models of complex systems that are amenable to program analysis. In the context of self-driving cars, the key idea is to leverage synthesis to generate models of particular scenarios, such as making a right turn or passing a car in a freeway, that capture a large space of possible situations, but are narrow enough for verification of individual components against those scenarios to be tractable. In addition to the technology development, the work provides the opportunity for students and postdocs who were involved in the ExCAPE effort to collaborate closely with our industrial partners at Toyota and apply these ideas in an industrial setting.

该项目的目标是利用作为“计算机辅助程序工程探险（ExCAPE）：利用综合软件设计”项目的一部分开发的综合和自动推理技术，以帮助确保自动驾驶车辆的安全。自动驾驶汽车涉及感知、规划、控制和算法的组合，这些组合过于复杂，无法完全验证以保证完全的可靠性，但其目标是表明，在许多重要场景下，单个组件可以被验证正确工作。该项目的关键创新之一是表明合成技术在这项具有挑战性的任务中发挥作用。综合通常旨在生成一段行为满足某些约束的代码，但是ExCAPE项目演示了综合的一个重要应用：生成可用于程序分析的复杂系统的模型。在自动驾驶汽车的背景下，关键的想法是利用合成来生成特定场景的模型，比如右转或在高速公路上超车，这些模型可以捕获大量可能的情况，但足够窄，可以针对这些场景验证单个组件，从而易于处理。除了技术开发之外，这项工作还为参与ExCAPE项目的学生和博士后提供了与丰田的工业合作伙伴密切合作的机会，并将这些想法应用于工业环境。