Hybrid, Distributed, and Now Formally Verified

To use the model with default options, first click SETUP, then click GO-EFFICIENT. Detailed instructions are below.

An extended version of the paper with additional proofs can be found here.

To use KeYmaera to prove safety of the local lane control, first launch KeYmaera and then load llc.key.proof.

powered by NetLogo

view/download model file: dccs.nlogo

This model models the movement of cars on a highway. Each car follows a simple set of rules: it slows down (decelerates) if it is not safely following the car ahead, and speeds up (accelerates) as soon as it is safely behind the car ahead. This model is a visual aid for the paper "Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified." It demonstrates a concrete example of the models verified in section 6.

Click on the SETUP button to set up the cars at the beginning of the lane. Set the NUMBER-OF-CARS to change the number of cars on the road.

Click on GO-EFFICIENT to start the cars moving.

The MAX-ACCELERATION button sets the limit for how the cars may accelerate. (The unit for acceleration is miles per hour per second, so if you know a car can go from 0 to 60mph in 3 seconds, its acceleration may be entered as 60mph/3sec.) In the GO-EFFICIENT simulation, the cars will either accelerate at this maximum, brake in the range of MAX-BRAKING and MIN-BRAKING or coast if the car is stopped or has reached the MAX-SPEED if SPEED-LIMIT is enabled.

The length of the lane may be changed with LANE-LENGTH. The cars will get very small and difficult to see, but the plots will become more interesting.

The RANDOM-SETUP starts the cars in random positions. The GO-RANDOM simulation allows the cars to choose any safe acceleration.

While you experiment with this model, it is important to remember that this is just an example of what has been verified. For instance, the frequent and drastic changes in acceleration would be terrible for passanger comfort. However, the verification proves safety for a large range of models, so a model which follows the overall safety parameters and gives a smooth ride by choosing a more graudaul acceleration is also verified. This demo is provided only as a visual aid.

The cars tend to platoon when they start out in groups and are given a long enough lane to reach the speed limit. This behavior is not programmed in, but rather happens automatically, so verification of this emergent behavior is also automatic. If you choose to SEE-PLATOONS, the cars will change color when they are driving at the speed-limit. If you reduce the speed limit and lengthen the lane, the platoons are more likely to form.

(Note: With a speed-limit of 45mph and default acceleration and braking, it takes 10 cars approximately 14 seconds to form a platoon.)

The plots show three values of the red and green cars as the model runs:

- the position of the car

- the speed of the car (this doesn't exceed the speed limit when the limit is enabled)

- the acceleration of the car (this is plotted point-wise since the value is not continuous)

A single time tick is equivalent to 1/100th of a second.

Our verification model proves the system for lanes with any (finite) length. To deal with the eventual end of a lane, we allow a "stopped car" to act as a permanent barrier, keeping the active cars from driving off the end of the road.

When running the GO-RANDOM simulation, cars will stop or slow down during the simulation. This allows us to observe traffic waves, which are not present in the efficient version.

globals [ hit-limit sample-car lead-car time maxr maxa maxb minb maxs lanel ] turtles-own [ speed speed-min leader acc eps prev-speed] to setup set lanel lane-length / 15 resize-world 0 lanel -4 4 set-patch-size min list ((50 / lanel) * 15.75) 15.75 clear-all ask patches [ setup-road ] set maxr (max-reaction * 100) set maxa (max-acceleration * 0.000009765) set maxb (max-braking * 0.000009765) set minb (min-braking * 0.000009765) set maxs (max-speed * 0.0009771) setup-cars-inorder end to random-setup set lanel lane-length / 15 resize-world 0 lanel -4 4 set-patch-size min list ((50 / lanel) * 15.75) 15.75 clear-all ask patches [ setup-road ] set maxr (max-reaction * 100) set maxa (max-acceleration * 0.000009765) set maxb (max-braking * 0.000009765) set minb (min-braking * 0.000009765) set maxs (max-speed * 0.0009771) setup-cars-randomly end to random-acc-setup clear-all ask patches [ setup-road ] setup-random-acc end to setup-road ;; patch procedure if ( pycor < 2 ) and ( pycor > -2 ) [ set pcolor white ] set time 0 end to setup-cars-inorder if ( number-of-cars > world-width ) [ user-message (word "There are too many cars for the amount of road. Please decrease the NUMBER-OF-CARS slider to below " (world-width + 1) " and press the SETUP button again. The setup has stopped.") stop ] set-default-shape turtles "car" repeat number-of-cars [ crt 1 [ set color blue setxy random-xcor 0 set heading 90 set speed random-float .005 ;; initial speed has a max val so all cars will fit. set speed-min 0 set acc ((0 - maxb) + (random-float (maxb + maxa))) ] ] set sample-car (turtle (random (number-of-cars - 2))) ask sample-car [ set color red ] set lead-car (turtle (number-of-cars - 2)) ask lead-car [ set color green ] let i number-of-cars - 1 ask turtle i [ set leader nobody setxy max-pxcor 0 set speed 0 set acc 0 ] ; set cars stopped and lined up at the starting line repeat number-of-cars - 1 [ set i i - 1 ask turtle i [ set leader turtle (i + 1) setxy i 0 set speed 0 set acc 0 ] ] end to setup-cars-randomly if ( number-of-cars > world-width ) [ user-message (word "There are too many cars for the amount of road. Please decrease the NUMBER-OF-CARS slider to below " (world-width + 1) " and press the SETUP button again. The setup has stopped.") stop ] set-default-shape turtles "car" repeat number-of-cars [ crt 1 [ set color blue setxy random-xcor 0 set heading 90 set speed random-float .005 ;; initial speed has a max val so all cars will fit. set speed-min 0 set acc ((0 - maxb) + (random-float (maxb + maxa))) ] ] set sample-car (turtle (random (number-of-cars - 2))) ask sample-car [ set color red ] let i number-of-cars - 1 ask turtle i [ set leader nobody setxy max-pxcor 0 set speed 0 set acc 0 ] ; set cars stopped in random position let n number-of-cars - 1 create-cars-rand-pos n min-pxcor (max-pxcor - 1) 0 ask turtles [ if who != number-of-cars - 1 [ set leader turtle (who + 1) set speed 0 set acc 0 ] ] set lead-car ([leader] of sample-car) ask lead-car [ set color green ] end to setup-random-acc if ( number-of-cars > world-width ) [ user-message (word "There are too many cars for the amount of road. Please decrease the NUMBER-OF-CARS slider to below " (world-width + 1) " and press the SETUP button again. The setup has stopped.") stop ] set-default-shape turtles "car" repeat number-of-cars [ crt 1 [ set color blue setxy random-xcor 0 set heading 90 set speed random-float .005 ;; initial speed has a max val so all cars will fit. set speed-min 0 set acc ((0 - maxb) + (random-float (maxb + maxa))) ] ] set sample-car (turtle (random (number-of-cars - 1))) ask sample-car [ set color red ] let i number-of-cars - 1 ask turtle i [ set leader nobody setxy max-pxcor 0 set speed 0 set acc 0 ] ;; set up cars with random starting acc and speed set hit-limit 0 repeat number-of-cars - 1 [ set i i - 1 ask turtle i [ set leader turtle (i + 1) ;create-link-to leader let safe-limit (([xcor] of leader) - 1 - ((speed ^ 2) / (2 * minb)) + ((([speed] of leader) ^ 2) / (2 * maxb)) - ((maxa / minb) + 1) * ((maxa / 2) * (maxr ^ 2) + maxr * speed)) set safe-limit min (list safe-limit ([xcor] of leader - 1)) if-else i < (safe-limit - (max-pxcor / number-of-cars)) and hit-limit = 0 ; lower limit of pos of car must be ahead of i, else not room for all cars on road [ set-car-pos (safe-limit - (max-pxcor / number-of-cars)) safe-limit ] ;set-car-pos i safe-limit ] [ setxy i 0 set speed 0 set acc 0 set hit-limit 1 ] ] ] end to create-cars-rand-pos [n lower upper i] if n != 0 [ if-else n = 1 [ ask turtle i [ setxy ((upper + lower) / 2) 0 ] ] [ let mid (lower + random-float (upper - lower)) if (mid - lower) < (ceiling (n / 2)) [set mid ((ceiling (n / 2)) + lower)] if (upper - mid) < (floor (n / 2)) [set mid (upper - (floor (n / 2)))] ;set mid ((upper + lower) / 2) create-cars-rand-pos (ceiling (n / 2)) lower mid i create-cars-rand-pos (floor (n / 2)) mid upper (i + (ceiling (n / 2))) ] ] end to set-car-pos[lower upper] let rand random-float (upper - lower) set rand rand + lower ;show rand setxy rand 0 end ;; this procedure is needed so when we click "Setup" we ;; don't end up with any two cars on the same patch to separate-cars ;; turtle procedure if any? other turtles in-radius 1 [ setxy random-xcor 0 ;fd 1 separate-cars ] end to go-random ask turtles [ if eps >= (1 / maxr) or (random-float 1) < .01 ;eps = random (1 / maxr) [ set eps 0 if who != (number-of-cars - 1) [ let safe-limit (([xcor] of leader) - 1 - ((speed ^ 2) / (2 * minb)) + ((([speed] of leader) ^ 2) / (2 * maxb)) - ((maxa / minb) + 1) * ((maxa / 2) * (maxr ^ 2) + maxr * speed)) if-else xcor < safe-limit ;[ set-car-acc (0 - maxb) maxa ] [ if (((ceiling time * 100) mod 300) = 0) [set-car-acc 0 maxa if ((random-float 1) < .05) [set-car-acc (0 - maxb) 0 ]] ] [ set-car-acc (0 - maxb) (0 - minb) ] move-car if speed < 0 [ set speed 0 set acc 0 ] if speed-limit [ if speed >= maxs [ set speed maxs set acc 0 ] ] ] ] ] ask turtles [ set eps eps + 1 fd speed ] tick plot-cars plot-cars2 if (max [speed] of turtles) = 0 and time > 6 [ stop ] end to go-efficient ask turtles [ if eps >= (1 / maxr) or (random-float 1) < .08 ;eps = random (1 / maxr) [ set eps 0 if who != (number-of-cars - 1) [ let safe-limit (([xcor] of leader) - 1 - ((speed ^ 2) / (2 * minb)) + ((([speed] of leader) ^ 2) / (2 * maxb)) - ((maxa / minb) + 1) * ((maxa / 2) * (maxr ^ 2) + maxr * speed)) if-else xcor < safe-limit [ set acc maxa ] [ set-car-acc (0 - maxb) (0 - minb) ] move-car if speed < 0 [ set speed 0 set acc 0 ] if speed-limit [ if-else speed >= maxs [ set speed maxs set acc 0 if see-platoons [set color pink]] [ if see-platoons [ if-else self = sample-car [set color red] [ if-else self = lead-car [set color green] [set color blue] ] ] ] ] ] ] ] ask turtles [ set eps eps + 1 fd speed ] tick plot-cars plot-cars2 if (max [speed] of turtles) = 0 and time > 2 [ stop ] end to set-car-acc[lower upper] let rand random-float (upper - lower) set rand rand + lower set acc rand end to move-car set speed (speed + acc) end to plot-cars set time time + .01 set-current-plot "Red Car" set-current-plot-pen "Position" plot [xcor] of sample-car set-current-plot-pen "Velocity" plot ([speed] of sample-car) * (1 / 0.0009771) set-current-plot-pen "Acceleration" plot ([acc] of sample-car) * (1 / 0.000009765) ;set-plot-x-range (time - 200) time end to plot-cars2 set-current-plot "Green Car" set-current-plot-pen "Position" plot [xcor] of lead-car set-current-plot-pen "Velocity" plot ([speed] of lead-car) * (1 / 0.0009771) set-current-plot-pen "Acceleration" plot ([acc] of lead-car) * (1 / 0.000009765) end