# Safety Verification of Driving Resource Occupancy Rules Based on Functional Language
## 4 CSP\({}_{\text{M}}\) Definition
### Analysis of Resource Occupation Rules  
The position time migration system of CCSP is obtained by expanding the position factor on the time migration system of CSP, and its state space can construct a reachable graph \(G\). \(G\):=(\(NODES\),\(EDGES\)), \(NODES\) = \(\{N_{i}\mid N_{i}\) is the node where the process executes, \(0\leq I\)\(\leq\)\(n\)], \(EDGES\) = [e(i,j) ] \(e(i,j)\) represents a directed edge from \(N_{i}\) to \(N_{j}\),\(0\leq i\leq n\), \(0\leq j\leq n\), and \(I\
eq j\)]. The inspection of resource occupation rules needs to check whether multiple entities at a certain moment will be in the same segment. In this paper, to solve this problem, on the basis of the state space graph \(G\), we judge whether \(G\) is a canonical reachable graph, that is, whether all the paths of the state space can satisfy the different segment spaces occupied at the same time. A resource occupancy rule security satisfiability check algorithm is used to determine whether \(G\) is a standardized reachability graph. In this algorithm, we set the current time to \(t\), use _set_path_ to store the visited path, and _abnormal_ to store the abnormal node. The Algorithm 1 details are as follows:```
Initialization:_time:= \(t\); abnormal:= \(\varnothing\); set_patht:= [\(N_{0}\)]; total:= 0; Repeat \(\mathit{hr}\):= last node in set_path; // take the last node of the current path If successor nodes of last node have been visited; // delete visited child nodes Then delete last node of set_path; total:= total - curr_t; // when deleting the last node, the total time must be subtracted from the relevant edge Else Begin \(\mathit{bn}\):= take a unvisited successor node of \(\mathit{ln}\); // take a child node \(\mathit{bn}\) of \(\mathit{ln}\) that has not been visited total:= total + curr_t; result:= true; \(\mathit{lk}_{\mathit{ln}}=\mathit{k}_{\mathit{ln}}\) then result:= false; // if the time is the same in the same segment \(k\), there is a danger abnormal = abnormal \(\cup\)[\(\mathit{en}\)]; Else \(\mathit{sel\_path}\):= set_path \(\cup\)[\(\mathit{bn}\)]; End Until set_path = \(\varnothing\); If abnormal = \(\varnothing\)then Return true; Else return false;
```

**Algorithm 1**

The input of this algorithm is graph \(G\), and the output is whether graph \(G\) satisfies the security occupancy rules of the segment. If the algorithm is satisfied, the return value is true, otherwise the return value is false. ## 5 Abstraction of the Environmental Model

The single-loop model is a typical autonomous driving scenario. We take the single-loop as an example to realize the abstraction of the environment model. As shown in Figure 2, we abstract the single-loop model. Figure 2: Single-loop diagram. **Definition 7**. : _Environment. The environment is a section of autonomous driving environment, including the static environment and dynamic environment of autonomous driving. For example, the big tree on the roadside is the static environment, and the moving car belongs to the dynamic environment. In this paper, the single ring road and the car running in it are an environment._

**Definition 8**. : _Segment. The roads included in the environment can be divided into several segments, as shown in Figure 2. The segments of single ring roads are [a1,a2,b,c1,c2,d,e1,e2,f,g1,g2,h,i,j,k,l,m,n,o,p]._

**Definition 9**. : _Arc. The line segment connecting two adjacent segments is an arc, and some arcs are drawn in the Figure 2. For example, if a1 is connected with a2, a1a2_ represents the arc of segment a1 and a2, connecting segments a1 and a2._

**Definition 10**. : _Route. The route is a segment that does not violate traffic rules and is composed of several adjacent arcs. For example, in the Figure 2, j->a2->b->c1->k is a route._

**Definition 11**. : _Car. The moving objects that appear in the scene are marked as car and numbered in the corresponding order. In the Figure 2, the three moving objects are car1, car2 and car3._

**Definition 12**. : _Scene._

1. _Collision The cars are in the same segment at the same time.