Safety Verification of Driving Resource Occupancy Rules Based on Functional Language

Autonomous driving is a safety-critical system, and the occupancy of its environmental resources affects the safety of autonomous driving. In view of the lack of safety verification of environmental resource occupation rules in autonomous driving, this paper proposes a verification method of automatic driving model based on functional language through CSPM. Firstly, the modeling and verification framework of an autopilot model based on CSPM is given. Secondly, the process algebra definition of CSPM is given. Thirdly, the typical single loop environment model in automatic driving is abstracted, and the mapping method from automatic driving model to CSP is described in detail for the automatic driving environment and the typical collision, overtaking, lane change and other scenes involved. Finally, the autopilot model of the single loop is mapped to CSPM, and the application effect of this method is discussed by using FDR tool. Experiments show that this method can verify the safety of autonomous driving resources, thereby improving the reliability of the autonomous driving model.