# Safety Verification of Driving Resource Occupancy Rules Based on Functional Language
## 4 CSP\({}_{\text{M}}\) Definition
### Analysis of Resource Occupation Rules
Driving car1 enters the single ring road from segment \(j\), car2 enters the single ring road from segment \(n\), and car3 enters the single ring road from segment _l_:

\(CARS1=CAR1\)\([\)\(\)\(\{\}\)\(\{\}\)\(\cup\)\(\cup\)\(\cup\)\(CAR2\)

\(CARS2=CARS1\)\([\)\(\{\}\)\(\{\}\)\(\cup\)trace(CAR3)\(\subseteq\)trace(CARS2) trace(CARS1)\(\subseteq\)trace(CARS2) The result of model checking is shown in Figure 3. The results obtained by inputting the above four security statements into the FDR tool are displayed as Passed, which conforms to the security attribute verification of the formal model. Figure 3: Safety inspection diagram. The deadlock-free results are as follows:

_assert CARS1:[deadlock free [F]]_

_assert CARS2:[deadlock free [F]]_

This assertion indicates that the processes _CARS1_ and _CARS2_ are deadlock-free. For example, for the process _CARS2_, _CARS2_ no deadlock indicates that for any trace \(s\), (\(s\), \(\sum\
otin\)_failures(CARS2)_. We input the processes CARS1 and CARS2 into FDR, and the result shows Passed, indicating that the two processes have no deadlock situation. That is, in this single-loop scenario, car1, car2 and car3 occupy segment resources to execute corresponding processes without causing deadlock. The above experimental results in Figure 4 show that all processes have passed the FDR model checking, indicating that the CSPM model of the autonomous driving environment has extremely high reliability, and meets the characteristics of safety and deadlock-free. Next, we need to check whether the car will be in the same segment at the same time, that is, whether there will be a collision. Since the segment is defined as a unit segment, that is, only one car is allowed to enter in a segment at the same time. Then the definition of collision is that, in the same time period, the segment occupied by the vehicle is the same segment. We represent the state space diagrams of Car1 and Car2, as shown in Figures 5 and 6. Figure 4: Deadlock-free diagram. Figure 5: State space of _Car1_. Figure 6: State space of _Car2_. Figure 5 shows the CAR1 process, that is, the state diagram of Car1. The nodes represent the current state, and there are corresponding edges between the nodes. The edges are marked with (t, frag), indicating the duration t and the segment name frag to enter the next segment. The four branches in the state diagram are the four paths for Car1 to enter the scene. Figure 6 is the CAR2 process, that is, the Car2 state diagram. The representation and meaning of its edges are the same as those in Figure 5, that is, the duration t and the segment name frag to enter the next segment are marked. The four branches in the state diagram are the four paths for Car2 to enter the scene. Analyze the segments that may be occupied by _Car1_ and _Car2_ through the analysis of resource occupancy in the state space. For example, segment \(d\) will be occupied from \(N_{24}\) to \(N_{25}\), and segment \(d\) will also be occupied from \(M_{50}\) to \(M_{51}\). The current time is 1. We use the resource security occupation checking algorithm to calculate that the occupation time of node \(N_{25}\) in _Car1_ for segment \(d\) is 11 and that of node \(N_{25}\) in _Car2_ for segment \(d\) is 22. Therefore, _Car1_ and _Car2_ will not occupy segment \(d\) at the same time. Therefore, the security occupation rules of resources are met. Check the occupancy of other segments in turn to detect the safe occupancy of resources. ## 7 Summary and Outlook

This paper combines the autonomous driving model with the functional language CSPM to verify the resource occupancy rules in autonomous driving scenarios. The scene is abstracted into multiple fragments, and the typical collision, overtaking, lane change and other scenes of automatic driving are abstracted into the occupation and operation of fragment resources. The scene is actually modeled as simpler segments, and the driving behavior of the vehicle is modeled as the operation of the segment, on this basis, the whole process of automatic driving is verified.