# Safety Verification of Driving Resource Occupancy Rules Based on Functional Language
## 4 CSP\({}_{\text{M}}\) Definition
### Analysis of Resource Occupation Rules
For example, at the same time, car1 and car2 are both in the f segment, which is a collision._
2. _Overtake For multiple roads, the car behind overtakes the car in front. Overtaking is not allowed in the single ring road in this paper._
3. _Lane change Drive to other lanes while driving. Lane changes are not allowed in the single ring road in this paper._
4. _Message transmission Message transmission refers to the signal transmitted by the signal lights of the preceding vehicle during driving. For example, if the right turn signal of the vehicle in front is turned on, the signal is transmitted and the vehicle in front will turn right._

## 6 Mapping Method from Autonomous Driving Decision Language to CSP\({}_{\text{M}}\) Language

Next, we map the autonomous driving environment to the CSP, and we divide the process into environment mapping and autonomous vehicle mapping. To simplify the model, this paper only considers several typical driving behaviors in autonomous driving: collision, overtaking and lane change. ### Environment Mapping

1. Segment. In the autonomous driving environment, the segment variable of the highway is mapped to the event variable in CSP. 2. Arc. Arcs are mapped to the order of execution of events in the process. For example, \(a\overset{\sim}{1}a2\) is mapped to execute \(a1\) first before executing \(a2\). 3. Car. The driving path of the car is mapped to a process and executed synchronously in the driving environment according to certain rules in the environment. For example, the driving path \(j\)->a2->b->c1->k of car2 can be mapped to process \(CAR2=j\)->a2->b->c1->k->STOP. 4. Other environment. Any road segment that is not in the environment is not considered, we only consider the road segment partially, and the road segment that is not in the environment is mapped as _STOP_ in the process. ### Autonomous Car Scene Mapping

1. Information transfer between vehicles, such as the right turn signal of the front vehicle, is mapped into communication between processes. 2. Vehicle collision, that is, occupying the same process resources at the same time or within a time period. 3. Vehicle lane change, that is, the change of driving path, is mapped to the change of execution sequence of events in the process. 4. Vehicles overtaking, that is, passing through other lanes. 5. Driving back to the original lane after changing lanes is also mapped to a change in the execution sequence of events in the process. ### Safety Verification of Resource Occupation in Driving Scenes

According to the above single-loop road map, the car can enter the single-loop road from four segments {_j,l,n,o_}. We take into account cars in four directions. channel _a1,a2,b,c1,c2,d,e1,e2,fg1,g2,h,i,j,k,l,m,n,o,p_

\(CAR1=j->((a2->b->c1->k->CAR1)\)

\([\)\((a2->b->c1->c2->d->e1->m->CAR1)\)

\([\)\((a2->b->c1->c2->d->e1->e2->f->g1->0->CAR1)\)

\([\)\((a2->b->c1->c2->d->e1->e2->f->g1->g2->h->a1->CAR1)\)

\(CAR2=n->((e2->f->g1->g1->0->CAR2)\)

\([\)\((e2->f->g1->g2->h->a1->i->CAR2)\)

\([\)\((e2->f->g1->g2->h->a1->a2->b->c1->k->CAR2)\)

\([\)\((e2->f->g1->g2->h->a1->a2->b->c1->c2->d->e1->m->CAR2)\)

\(CAR3=l->((c2->d->e1->m->CAR3)\)

\([\)\((c2->d->e1->e2->f->g1->0->CAR3)\)

\([\)\((c2->d->e1->e2->f->g1->g2->h->a1->i->CAR3)\)

\([\)\((c2->d->e1->e2->f->g1->g2->h->a1->a2->b->c1->k->CAR3)\)

\(CAR4=p->((g2->h->a1->i->CAR4)\)

\([\)\((g2->h->a1->a2->b->c1->k->CAR4)\)

\([\)\((g2->h->a1->a2->b->c1->c2->d->e1->m->CAR4)\)

\([\)\((g2->h->a1->a2->b->c1->c2->d->e1->m->CAR4)\)

\([\)\((g2->h->a1->a2->b->c1->c2->d->e1->e2->f->g1->0->CAR4)\)

\([\)\((g2->h->a1->a2->b->c1->c2->d->e1->e2->f->g1->0->CAR4)\)

We use Figure 2 as the scene to test the scenes of car1, car2, and car3.