# Safety Verification of Driving Resource Occupancy Rules Based on Functional Language
## 1 Introduction  
The development of the Automated Driving System (ADS) has been around for a long time, and the degree of intelligence has continued to increase after the 21 st century [1; 2; 3; 4; 5; 6]. Autonomous driving technology is an important research topic at present. Autonomous driving technology has many advantages. First of all, the automatic driving system is very intelligent and has high-efficiency computing power. It can accurately identify various parameters of the car when it is running, and the activity status of the surrounding cars, which can assist humans in grasping the driving environment. This is the first benefit of autonomous driving. The second benefit is that autonomous driving can enhance road safety. Now that the traffic is developed, the car ownership rate has been rising, and traffic accidents have been happening all the time, but 80% of the traffic accidents are caused by human factors. Further, autonomous driving technology excludes human factors and can effectively reduce road accidents. The third benefit is that autonomous driving technology can take advantage of the ecological environment. One of the best aspects of a self-driving car is that it uses electricity as its primary energy source. As a result, these cars are more environmentally friendly and cost less. In addition, self-driving cars do not emit any tailpipe, thus helping to reduce air pollution [7; 8; 9]. However, with the continuous development of autonomous driving, the safety issues of autonomous driving have gradually emerged [10; 11]. In 2016, a Model S car collided due to the fact that it did not recognize the white tractor ahead when the autopilot was turned on [12]. In 2018, an Uber car hit a pedestrian to death because it did not recognize the pedestrian in the shadow [13]. At present, the main causes of autonomous driving accidents are: violation of traffic rules,passive collisions and insufficient environmental perception information [14]. Among them, there are many accident problems caused by insufficient environmental information perception, and the autonomous driving environment has uncertain factors, for example, it is affected by current roads or other vehicles. The current movement of vehicles has a certain degree of uncertainty. The problem of resource occupancy in autonomous driving scenarios also affects the safety of autonomous driving. Therefore, the safety verification of the resource occupation rules of automatic driving has also become a key issue to ensure the safety of automatic driving. The traffic situation of autonomous driving is complex, and the road is also very complex, so it is very necessary to extract scene information. The roundabout has a central island in the center of the intersection, and all vehicles entering the roundabout travel in a counterclockwise direction. The roundabout is an accident-prone area, and we chose the roundabout to study its safety. On the one hand, the roundabout scene is a complex form of straight road sections, and the research on the roundabout scene is representative to a certain extent, and the safety verification of the roundabout scene can also guide the safety research of other scenarios. On the other hand, due to the frequent occurrence of accidents in the roundabout, the safety is difficult to guarantee, and it has great research significance for the abstraction of the roundabout scene and the safety verification of the vehicle form. In a single-loop scenario, vehicles from multiple directions are often involved. How to coordinate the vehicles coming from multiple parties and ensure the safe driving of vehicles is also particularly important. Therefore, this paper uses the roundabout scenario to study the safety of autonomous driving. Formal methods are accurate and verifiable, have strict mathematical language and strict mathematical semantics, and can model and verify the system. It originated from the program verification of Dijkstra and Hoare, which is convenient for machine support and automatic processing [15].