Principal Investigator

Rahul Mangharam

Status

Completed

Start Date

Jan. 1, 2016

End Date

Dec. 31, 2016

Project Type

Research Advanced

Grant Program

MAP-21 TSET National (2013 - 2018)

Grant Cycle

TSET - University of Pennsylvania

Visibility

Public

Abstract

APEX: Autonomous Vehicle Plan Verification and Execution: Autonomous vehicles (AVs) have already driven millions of miles on public roads, but even the simplest scenarios, such as a lane change maneuver, have not been certified for safety. This is a significant problem as the insurance liability of autonomous vehicles currently is entirely on the manufacturer as there is no systematic method to bound and minimize the risk of decisions made by the vehicle’s decision controller. Current methodologies for the verification of AV's decision and control systems attempt to divorce the lower level, short-term trajectory planning and trajectory tracking functions from the behavioral rules-based framework that governs mid-term actions. We are developing APEX, a tool for verification and execution of autonomous vehicle planning and control decisions across a variety of driving scenarios. 
    

Description

The APEX verification tool investigates the combined action of a behavioral planner and state lattice-based motion planner to guarantee a safe vehicle trajectory is chosen. In APEX, decisions made at the behavioral layer can be traced through to the spatio-temporal evolution of the AV and verified. Thus, there is no need to create abstractions of the AV’s controllers, and aggressive trajectories required for evasive maneuvers can be accurately investigated. In APEX, decisions made at the behavioral layer can be traced through to the spatio-temporal evolution of the AV and verified. Recent work includes: 

(a) A simulation environment for autonomous vehicles (AVs), which allows the creation of scenarios like intersections and highways. 
(b) Implementation of a state lattice local planner and trajectory generator. Including validation of the algorithm on a real Prius and in simulation.
(c) Creation of an agile reduced-scale AV is being developed. Equipped with a camera, an optical flow sensor and a LIDAR, this AV will serve as the experimental testbed on which verified control algorithms will be run.

Timeline

The project has a 1 year term

Strategic Description / RD&T

Deployment Plan

Methodology:
1) APEX: Our main contribution is an approach to formally verifying the trajectory planning and trajectory tracking stacks of an ADAS/AV. This approach is implemented in a software tool, APEX, and illustrated with examples of a lane change maneu- ver. The verification approach has two characteristics: 
a.	It is formal: we are guaranteed that if APEX determines a scenario to be safe, then it is safe. No amount of simulation can find an unsafe behavior in a scenario verified as correct by APEX. 

b.	It allows the use of an arbitrary trajectory planner, includ- ing one that only exists as code. That is, there is no need to model the trajectory planner, which is often very complex software. Moreover, the same trajectory planner can then be run on a real vehicle. APEX uses a trajectory planner that has been tested on a real vehicle. 

c.	In APEX, the verification engineer can

• Specify the low-level dynamics of the vehicle, including 
the trajectory tracker. These can be nonlinear. The default model in APEX is a 7D bicycle model. 

•	Provide a motion planner that takes in a starting position and end position and returns a trajectory that links the two points. The motion planner can be any piece of software: there are no restrictions on it. The default planner in APEX is a state lattice planner incorporated in ROS and tested on a real vehicle. 

•	Specify a sequence of goal positions (or waypoints) that the vehicle must visit, or a behavioral planner that com- putes these waypoints in a reactive manner. The default behavioral planner in APEX is a simple 2-state automaton that decides whether to do lane following or lane changing. 

•	Specify the uncertainty sets for the ego vehicle and the other agents in the scenario. 

•	Specify the unsafe conditions to be avoided by the vehi- cle. APEX supports a rich specification language (namely, Linear Temporal Logic) for describing unsafe behaviors. 


APEX will then verify, in an exhaustive fashion, that the ego vehicle can complete the scenario under the specified uncer- tainty, or return a specific case where it fails. The engineers can then use this counter-example in order to debug the controllers, and better understand how to avoid this failure. APEX is to be used at design-time by the verification engineers. It will allow them to quickly make modifications to the car’s controllers, and exhaustively verify the scenarios of interest. 

Expected Outcomes/Impacts

APEX is a tool for formally verifying the trajectory planning and tracking stacks of ADAS/AV cars, and is available for download. It can perform formal verification on realistic au- tonomous vehicle planning stacks. Future work will incorpo- rate more complex behavioral controllers for other scenarios, including synthesized planners, and will add a GUI to the tool.

Partnerships:
We are currently pursuing potential collaborations with industry to produce a deployable prototype on a Toyota Prius. We have the support of Toyota ITC, Mountain View, CA. We also have stong collaboration on the AV software from Nagoya University. Continued funding should help realize the development of such a prototype.

Expected Outputs

TRID

Individuals Involved

Email	Name	Affiliation	Role	Position
rahulm@seas.upenn.edu	Mangharam, Rahul	University of Pennsylvania	PI	Other

Budget

Amount of UTC Funds Awarded

$127500.00

Total Project Budget (from all funding sources)

$

Documents

Type	Name	Uploaded
Final Report	27_-_Mangharam.docx	July 16, 2018, 4:37 a.m.

Match Sources

No match sources!

Partners

No partners!