Good morning everyone, the topic of my speech is Formal Modeling Of Driverless Cars Overtaking Behavior In Highway
I divided the report into four parts, they are：Background、Technical route: Event-B、Modeling、Results And Conclusion
Let's go to the first part:Background。

There is a driverless car in this picture.
Laser radar system installed on the top of the car
And it has the function of ranging and positioning
Driverless cars have six modules to control it they are
For example turn left turn right tracking and braking.
This is a schematic diagram of the overtaking behavior model of a driverless car.
Let's go to the second part:Technical route: Event-B
What is Event-B?
What is formal method?
In the field of computer science and software engineering, the formal method is a special technique based on mathematics, suitable for the description, development and verification of software and hardware
systems.
What does it do in real world?
Let's go to the third part: Modeling
These pictures show us how the driverless car works.
In my model, I first initialized two cars and six areas, and the speed of the rear car is greater than the previous car, as shown in the previous picture
When there is no car in area 3 and 6 ,then you can overtake to the left.
If the area 6 has a car, but the speed of the area 6 car is greater than the speed of the area 2, still turn left overtaking
If the speed of the car in area 6 is less than the speed of the car in area 2, and follow the car.
If the area 3 has a car, and the car passing through the calculation area 1 must collide with the car of the area 2, it will overtake from the right side
This is just a brief introduction, the actual modeling situation is more complicated than this
Let's go to the four part:Results and conclusion
Using Event-B software, the model finally passed the certification, and obtained the certification obligation of all 108 certificates.
In this paper, event-b method was used to explore the modeling in the field of intelligent information, and a system model of driverless cars overtaking on highways was built。