Safety Mechanism Design and Verification of Safety Computer Parallel Program

The extensive application of Commercial off-the-shelf (COTS) components into safety computers in train control systems has caused safety problems. Aiming at the parallel programs, a concurrent program safety management mechanism based on transactional memory is proposed. The proposed mechanism implements concurrent behaviors of the application in the safe policy. A verification framework based on invariant proof and parallel separation logic theory is designed and operating system operation semantics are given for mathematical reasoning and proving. An example of code execution process is demonstrated to explain the safety control process of concurrent safety mechanism. The results indicate that the program can meet the safety and reliability requirements of concurrent safety computer platforms.