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项目证明了合成的重要应用：生成可以适应程序分析的复杂系统模型。在自动驾驶汽车的背景下，关键的想法是利用合成来生成特定场景的模型，例如进行正确的转弯或在高速公路中驾驶汽车，以捕获可能情况的较大空间，但足够狭窄，可以验证各个组件在这些方案上可以验证这些情况。除了技术开发外，这项工作还为参与与我们在Toyota的工业合作伙伴紧密合作并在工业环境中运用这些想法的学生和博士后为学生提供了机会。