File preview
8/2/2011
GM-Carnegie Mellon Autonomous Driving CRL
Advanced Transportation Systems
Raj Rajkumar
Electrical & Computer Engg.
Andre Platzer
Computer Science
Ed Clarke
Computer Science
Paul Rybski
Robotics Institute
John Dolan
Robotics Institute
David Wettergreen
Robotics Institute
Paolo Zuliani (CS)
GM-Carnegie Mellon Autonomous Driving CRL
Society and Automobiles
• More than 1 million people die every year in automotive accidents globally
– Largest global killer of aged 10-24 – Tens of millions of injuries – Global annual cost of road injuries in medical care, disability and property damage is $518 billion.
• Loss of independence and self-esteem of senior and disabled citizens • Traffic delays are expensive.
– The average US driver spends a week stuck in traffic per year. – In the EU, 80 billion euros wasted per year due to traffic congestion.
Build scientific and technological foundations to make transportation systems safer and more autonomous.
1
8/2/2011
GM-Carnegie Mellon Autonomous Driving CRL
Autonomous Vehicles?
GM-Carnegie Mellon Autonomous Driving CRL
Challenges and Approach
2
8/2/2011
GM-Carnegie Mellon Autonomous Driving CRL
Sarah Loos and André Platzer
Hybrid Systems Verification
GM-Carnegie Mellon Autonomous Driving CRL
Compositionality and Reconfiguration for Distributed Hybrid Systems
Hierarchical Modularity Nonlinear Dynamics
¬F F
3
8/2/2011
GM-Carnegie Mellon Autonomous Driving CRL
How Can We Prove Safety on Highways? !
GM-Carnegie Mellon Autonomous Driving CRL
Car Adaptive Cruise Control: Proof Sketch
Quantified Differential Dynamic Logic
Local Lane Control
Global Lane Control
Local Highway Global Highway Control Control
2 vehicles 1 lane no lane change
n vehicles 1 lane no lane change
n vehicles 1 lane Lane changes
n vehicles m lanes Lane changes
Sarah M. Loos, André Platzer, and Ligia Nistor, “Adaptive cruise control: Hybrid, distributed, and now formally verified”, In Michael Butler and Wolfram Schulte, editors, 17th Int’l Symp on Formal Methods, FM, Limerick, Ireland, Proceedings, Springer, 2011.
4
8/2/2011
GM-Carnegie Mellon Autonomous Driving CRL
Matthias Althoff & John Dolan
Reachability Analysis
GM-Carnegie Mellon Autonomous Driving CRL
Behavioral Threat Assessment
Autonomous vehicles cannot perfectly follow planned trajectories due to Modeling uncertainties Uncertain measurements Disturbances
5
8/2/2011
GM-Carnegie Mellon Autonomous Driving CRL
Behavioral Threat Assessment
Autonomous vehicles cannot perfectly follow planned trajectories due to Modeling uncertainties Uncertain measurements Disturbances Consequence: Planned maneuver is safe under perfect conditions, but may become unsafe due to uncertainties Objective: Guarantee safety when bounds on uncertainties are known
GM-Carnegie Mellon Autonomous Driving CRL
Threat Assessment – Reachable Sets
In general, the set of reachable states cannot be computed exactly.
6
8/2/2011
GM-Carnegie Mellon Autonomous Driving CRL
Threat Assessment – Reachable Sets
In general, the set of reachable states cannot be computed exactly We compute an over-approximation Guarantees that the real system is safe, but may lead to spurious counterexamples
GM-Carnegie Mellon Autonomous Driving CRL
Threat Assessment – Example
au
Prevent: Hitting the pedestrian Colliding with the oncoming vehicle Leaving the road boundaries
7
8/2/2011
GM-Carnegie Mellon Autonomous Driving CRL
Threat Assessment – Example
Reachable set
Initial states
Vehicle parameters from a 1986 Pontiac 6000 STE sedan The white set shows the set of initial states Black lines show example simulation results
GM-Carnegie Mellon Autonomous Driving CRL
Threat Assessment – Example
-5
Computation time in MatLab on a 1.6-GHz Intel i7 processor: Reachable set computation: 2.24 s (taking advantage of parallelization) Occupancy set computation: 0.46 s Collision check: 0.25 s Overall time by interleaving processes: 2.24 s Around 2 times faster than real-time (maneuver time: 5 s)
Matthias Althoff & John M. Dolan, “Set-Based Computation of Vehicle Behaviors for the Online Verification of Autonomous Vehicles,” to appear in Proc. 14th Intl. IEEE Conf. on Intelligent Transportation Systems, Washington, D.C., Oct. 5-7, 2011.
8
8/2/2011
GM-Carnegie Mellon Autonomous Driving CRL
Edmund Clarke and Paolo Zuliani
Statistical Model Checking
GM-Carnegie Mellon Autonomous Driving CRL
Probabilistic Verification
Verification of stochastic system models via statistical model checking Temporal logic specifications:
= “in the next 20 minutes, the system is unavailable for at least 1 sec.”
Two questions
What is Prob ( )?
Answer: simulation + model checking + statistical estimation
Is Prob ( ) > θ ?
Answer: simulation + model checking + statistical hypothesis test
Efficient Bayesian estimation and hypothesis test techniques
9
8/2/2011
GM-Carnegie Mellon Autonomous Driving CRL
Probabilistic Verification
Applications: Verification of Stateflow/Simulink models
Example:
= ¬F100 G1(FuelFlowRate = 0) Prob ( ) = 0.9779 ± .01
Work in progress: rare events
Too many simulations required when Prob( ) is small Solution: use importance sampling to bias samples Using cross entropy to select a good biasing function
GM-Carnegie Mellon Autonomous Driving CRL
Importance Sampling
The fundamental Importance Sampling identity
density of X
biasing density
likelihood ratio
10
8/2/2011
GM-Carnegie Mellon Autonomous Driving CRL
Experiences with Technique
• Fault-tolerant fuel control system (SF/SL)
– Faulty sensors (Poisson processes) • = F100 G1(FuelFlowRate = 0), Prob( )<<1
• Preliminary results using
– 10,000 samples for Cross Entropy – 100,000 samples for importance sampling
• Probability estimate of Prob( ) in the order of 10-15 (relative error =13%) • Infeasible with crude Monte Carlo technique
GM-Carnegie Mellon Autonomous Driving CRL
Hyunggi Cho and Paul Rybski
Bicycle Detection
11
8/2/2011
GM-Carnegie Mellon Autonomous Driving CRL
Detecting and Tracking Vulnerable Road Users
• Autonomous vehicles must be aware of and navigate around cars as well as vulnerable road users:
– Bicycles – Pedestrians – Motorcycles
•
•
•
Bicyclists must share urban road lanes with cars and move at comparable speeds Bicyclists are particularly unprotected against injury in a collision (e.g. no crumple zone) In 2009, 630 bicyclists were killed and 51,000 were injured in traffic accidents in the United States.*
http://www.youtube.com/watch?v=Dab48_0rYEU
*http://www-nrd.nhtsa.dot.gov/Pubs/811386.pdf
GM-Carnegie Mellon Autonomous Driving CRL
Detecting Moving Objects
Deformable Part Model – Histogram of Oriented Gradients (DPM- HOG) Algorithm
H. Cho, P. E. Rybski, W. Zhang, "Vision-based 3D Bicycle Tracking using Deformable Part Model and Interacting Multiple Model Filter," IEEE International Conference on Robots and Automation, May, 2011.
12
8/2/2011
GM-Carnegie Mellon Autonomous Driving CRL
Visual Bicycle Detection and Tracking from a Moving Vehicle
http://www.youtube.com/watch?v=oVfKS_qH068
GM-Carnegie Mellon Autonomous Driving CRL
Reza Azimi, Gaurav Bhatia and Raj Rajkumar
Vehicular Networks
13
8/2/2011
GM-Carnegie Mellon Autonomous Driving CRL
Intersection Management
Using V2V
With Traffic Lights
GM-Carnegie Mellon Autonomous Driving CRL
Intersection Mgmt Results
Significant overall performance improvement. Average delays: •V2V: 12.91806 s •10s traffic lights: 124.6954 s •30s traffic lights: 158.3727 s
14
8/2/2011
GM-Carnegie Mellon Autonomous Driving CRL
Next-Gen Autonomous Platform
Goal: Drive autonomously wherever/whenever the average person can drive in the US.
GM-Carnegie Mellon Autonomous Driving CRL
Conclusions
• Notable progress on
– Verification & Validation
• Stochastic Model Checking • Hybrid Systems • Reachability Analysis
– Vehicle-to-Vehicle Communications
• Inter-vehicle Cooperation
– Autonomous platform & infrastructure
• Sensors being integrated
• Future Work on Principles & Prototyping
– Fault-tolerance of resources (including sensors) – Real-time multicore scheduling – Safe behaviors at high speeds
15
GM-Carnegie Mellon Autonomous Driving CRL
Advanced Transportation Systems
Raj Rajkumar
Electrical & Computer Engg.
Andre Platzer
Computer Science
Ed Clarke
Computer Science
Paul Rybski
Robotics Institute
John Dolan
Robotics Institute
David Wettergreen
Robotics Institute
Paolo Zuliani (CS)
GM-Carnegie Mellon Autonomous Driving CRL
Society and Automobiles
• More than 1 million people die every year in automotive accidents globally
– Largest global killer of aged 10-24 – Tens of millions of injuries – Global annual cost of road injuries in medical care, disability and property damage is $518 billion.
• Loss of independence and self-esteem of senior and disabled citizens • Traffic delays are expensive.
– The average US driver spends a week stuck in traffic per year. – In the EU, 80 billion euros wasted per year due to traffic congestion.
Build scientific and technological foundations to make transportation systems safer and more autonomous.
1
8/2/2011
GM-Carnegie Mellon Autonomous Driving CRL
Autonomous Vehicles?
GM-Carnegie Mellon Autonomous Driving CRL
Challenges and Approach
2
8/2/2011
GM-Carnegie Mellon Autonomous Driving CRL
Sarah Loos and André Platzer
Hybrid Systems Verification
GM-Carnegie Mellon Autonomous Driving CRL
Compositionality and Reconfiguration for Distributed Hybrid Systems
Hierarchical Modularity Nonlinear Dynamics
¬F F
3
8/2/2011
GM-Carnegie Mellon Autonomous Driving CRL
How Can We Prove Safety on Highways? !
GM-Carnegie Mellon Autonomous Driving CRL
Car Adaptive Cruise Control: Proof Sketch
Quantified Differential Dynamic Logic
Local Lane Control
Global Lane Control
Local Highway Global Highway Control Control
2 vehicles 1 lane no lane change
n vehicles 1 lane no lane change
n vehicles 1 lane Lane changes
n vehicles m lanes Lane changes
Sarah M. Loos, André Platzer, and Ligia Nistor, “Adaptive cruise control: Hybrid, distributed, and now formally verified”, In Michael Butler and Wolfram Schulte, editors, 17th Int’l Symp on Formal Methods, FM, Limerick, Ireland, Proceedings, Springer, 2011.
4
8/2/2011
GM-Carnegie Mellon Autonomous Driving CRL
Matthias Althoff & John Dolan
Reachability Analysis
GM-Carnegie Mellon Autonomous Driving CRL
Behavioral Threat Assessment
Autonomous vehicles cannot perfectly follow planned trajectories due to Modeling uncertainties Uncertain measurements Disturbances
5
8/2/2011
GM-Carnegie Mellon Autonomous Driving CRL
Behavioral Threat Assessment
Autonomous vehicles cannot perfectly follow planned trajectories due to Modeling uncertainties Uncertain measurements Disturbances Consequence: Planned maneuver is safe under perfect conditions, but may become unsafe due to uncertainties Objective: Guarantee safety when bounds on uncertainties are known
GM-Carnegie Mellon Autonomous Driving CRL
Threat Assessment – Reachable Sets
In general, the set of reachable states cannot be computed exactly.
6
8/2/2011
GM-Carnegie Mellon Autonomous Driving CRL
Threat Assessment – Reachable Sets
In general, the set of reachable states cannot be computed exactly We compute an over-approximation Guarantees that the real system is safe, but may lead to spurious counterexamples
GM-Carnegie Mellon Autonomous Driving CRL
Threat Assessment – Example
au
Prevent: Hitting the pedestrian Colliding with the oncoming vehicle Leaving the road boundaries
7
8/2/2011
GM-Carnegie Mellon Autonomous Driving CRL
Threat Assessment – Example
Reachable set
Initial states
Vehicle parameters from a 1986 Pontiac 6000 STE sedan The white set shows the set of initial states Black lines show example simulation results
GM-Carnegie Mellon Autonomous Driving CRL
Threat Assessment – Example
-5
Computation time in MatLab on a 1.6-GHz Intel i7 processor: Reachable set computation: 2.24 s (taking advantage of parallelization) Occupancy set computation: 0.46 s Collision check: 0.25 s Overall time by interleaving processes: 2.24 s Around 2 times faster than real-time (maneuver time: 5 s)
Matthias Althoff & John M. Dolan, “Set-Based Computation of Vehicle Behaviors for the Online Verification of Autonomous Vehicles,” to appear in Proc. 14th Intl. IEEE Conf. on Intelligent Transportation Systems, Washington, D.C., Oct. 5-7, 2011.
8
8/2/2011
GM-Carnegie Mellon Autonomous Driving CRL
Edmund Clarke and Paolo Zuliani
Statistical Model Checking
GM-Carnegie Mellon Autonomous Driving CRL
Probabilistic Verification
Verification of stochastic system models via statistical model checking Temporal logic specifications:
= “in the next 20 minutes, the system is unavailable for at least 1 sec.”
Two questions
What is Prob ( )?
Answer: simulation + model checking + statistical estimation
Is Prob ( ) > θ ?
Answer: simulation + model checking + statistical hypothesis test
Efficient Bayesian estimation and hypothesis test techniques
9
8/2/2011
GM-Carnegie Mellon Autonomous Driving CRL
Probabilistic Verification
Applications: Verification of Stateflow/Simulink models
Example:
= ¬F100 G1(FuelFlowRate = 0) Prob ( ) = 0.9779 ± .01
Work in progress: rare events
Too many simulations required when Prob( ) is small Solution: use importance sampling to bias samples Using cross entropy to select a good biasing function
GM-Carnegie Mellon Autonomous Driving CRL
Importance Sampling
The fundamental Importance Sampling identity
density of X
biasing density
likelihood ratio
10
8/2/2011
GM-Carnegie Mellon Autonomous Driving CRL
Experiences with Technique
• Fault-tolerant fuel control system (SF/SL)
– Faulty sensors (Poisson processes) • = F100 G1(FuelFlowRate = 0), Prob( )<<1
• Preliminary results using
– 10,000 samples for Cross Entropy – 100,000 samples for importance sampling
• Probability estimate of Prob( ) in the order of 10-15 (relative error =13%) • Infeasible with crude Monte Carlo technique
GM-Carnegie Mellon Autonomous Driving CRL
Hyunggi Cho and Paul Rybski
Bicycle Detection
11
8/2/2011
GM-Carnegie Mellon Autonomous Driving CRL
Detecting and Tracking Vulnerable Road Users
• Autonomous vehicles must be aware of and navigate around cars as well as vulnerable road users:
– Bicycles – Pedestrians – Motorcycles
•
•
•
Bicyclists must share urban road lanes with cars and move at comparable speeds Bicyclists are particularly unprotected against injury in a collision (e.g. no crumple zone) In 2009, 630 bicyclists were killed and 51,000 were injured in traffic accidents in the United States.*
http://www.youtube.com/watch?v=Dab48_0rYEU
*http://www-nrd.nhtsa.dot.gov/Pubs/811386.pdf
GM-Carnegie Mellon Autonomous Driving CRL
Detecting Moving Objects
Deformable Part Model – Histogram of Oriented Gradients (DPM- HOG) Algorithm
H. Cho, P. E. Rybski, W. Zhang, "Vision-based 3D Bicycle Tracking using Deformable Part Model and Interacting Multiple Model Filter," IEEE International Conference on Robots and Automation, May, 2011.
12
8/2/2011
GM-Carnegie Mellon Autonomous Driving CRL
Visual Bicycle Detection and Tracking from a Moving Vehicle
http://www.youtube.com/watch?v=oVfKS_qH068
GM-Carnegie Mellon Autonomous Driving CRL
Reza Azimi, Gaurav Bhatia and Raj Rajkumar
Vehicular Networks
13
8/2/2011
GM-Carnegie Mellon Autonomous Driving CRL
Intersection Management
Using V2V
With Traffic Lights
GM-Carnegie Mellon Autonomous Driving CRL
Intersection Mgmt Results
Significant overall performance improvement. Average delays: •V2V: 12.91806 s •10s traffic lights: 124.6954 s •30s traffic lights: 158.3727 s
14
8/2/2011
GM-Carnegie Mellon Autonomous Driving CRL
Next-Gen Autonomous Platform
Goal: Drive autonomously wherever/whenever the average person can drive in the US.
GM-Carnegie Mellon Autonomous Driving CRL
Conclusions
• Notable progress on
– Verification & Validation
• Stochastic Model Checking • Hybrid Systems • Reachability Analysis
– Vehicle-to-Vehicle Communications
• Inter-vehicle Cooperation
– Autonomous platform & infrastructure
• Sensors being integrated
• Future Work on Principles & Prototyping
– Fault-tolerance of resources (including sensors) – Real-time multicore scheduling – Safe behaviors at high speeds
15