权益分类	功能权益	普通用户	{{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工作的学生和博士后提供了与我们在丰田的工业合作伙伴密切合作的机会，并将这些想法应用于工业环境。