Safety Mechanism Design and Verification of Safety Computer Parallel Program

作     者：ZHANG Yuzhuo HONG Chunhua CAO Yuan MA Lianchuan WEN Yinghong 

作者机构：School of Electronic and Information Engineering Beijing Jiaotong University National Engineering Research Center of Rail Traffic Control System Beijing Jiaotong University 

出 版 物：《Chinese Journal of Electronics》 (电子学报(英文))

年 卷 期：2018年第27卷第6期

页      面：1163-1169页

核心收录：

学科分类：08[工学] 082302[工学-交通信息工程及控制] 0823[工学-交通运输工程] 

基　　金：supported by the National Natural Science Foundation of China(No.U1534208,No.U1734211) the National Key R&D Program of China(No.2018YFB1201601) 

主　　题：Safety computer Parallel program Transactional memory Invariant proof Concurrent separation logic 

摘      要：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.