Safety Mechanism Design and Verification of Safety Computer Parallel Program

ZHANG Yuzhuo; HONG Chunhua; CAO Yuan; MA Lianchuan; WEN Yinghong

doi:10.1049/cje.2018.02.016

Volume 27 Issue 6

Turn off MathJax

Article Contents

Article Navigation > Chinese Journal of Electronics > 2018 > 27(6): 1163-1169

ZHANG Yuzhuo, HONG Chunhua, CAO Yuan, et al., “Safety Mechanism Design and Verification of Safety Computer Parallel Program,” Chinese Journal of Electronics, vol. 27, no. 6, pp. 1163-1169, 2018, doi: 10.1049/cje.2018.02.016

Citation:

ZHANG Yuzhuo, HONG Chunhua, CAO Yuan, et al., “Safety Mechanism Design and Verification of Safety Computer Parallel Program,” Chinese Journal of Electronics, vol. 27, no. 6, pp. 1163-1169, 2018, doi: 10.1049/cje.2018.02.016

Citation:

PDF( 334 KB)

Safety Mechanism Design and Verification of Safety Computer Parallel Program

doi: 10.1049/cje.2018.02.016

1.
School of Electronic and Information Engineering, Beijing Jiaotong University, Beijing 100044, China;
2.
National Engineering Research Center of Rail Traffic Control System, Beijing Jiaotong University, Beijing 100044, China

Funds: This work is supported by the National Natural Science Foundation of China (No.U1534208, No.U1734211) and the National Key R&D Program of China (No.2018YFB1201601).

More Information

Corresponding author: CAO Yuan (corresponding author) received the B.S. degree in electric engineering and automation from Dalian Jiaotong University and Ph.D. degree in traffic information engineering and control from Beijing Jiaotong University in 2004 and 2011 respectively, where he is now an associate professor. He has taken part in several key national research projects in the field of train control system. His research interests include formal verification and railway signal. (Email:ycao@bjtu.edu.cn)
Received Date: 2017-06-19
Rev Recd Date: 2017-09-13
Publish Date: 2018-11-10

Abstract

Abstract

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.
- Safety computer,
- Parallel program,
- Transactional memory,
- Invariant proof,
- Concurrent separation logic

FullText(HTML)

References(15)

References

X. Xu, Y. Lin and X. Yang, “Protocol-aware process placement for MPI programs”, Chinese Journal of Eletronics, Vol.23, No.4, pp.701-705, 2014.

A. Bouajjani and M. Emmi, “Analysis of recursively parallel programs”, ACM Sigplan Notices, Vol.47, No.1, pp.203-214, 2011.

T. Tian and D. Gong, “Evolutionary generation approach of test data for multiple paths coverage of message-passing parallel programs”, Chinese Journal of Eletronics, Vol.23, No.2, pp.291-296, 2014.

Y. Li, Y. Zhang, Y. Chen, et al., “Formal reasoning about lazySTM programs”, Journal of Computer Science and Technology, Vol.25,No.4, pp.841-852, 2010.

M. Sousa and I. Dillig, “Cartesian hoare logic for verifying k-safety properties”, ACM SIGPLAN Notices, Vol.51, No.6, pp.57-69, 2016.

Z. Yan, H. Jiang, D. Feng, et al., “SUV: A novel single-update version-management scheme for hardware transactional memory systems”, International Journal of Communication Systems, Vol.27, No.12, pp.4166-4184, 2013.

D. Aspinall, L. Beringer, M. Hofmann, et al.,“A program logic for resources”, Theoretical Computer Science, Vol.389, No.3, pp.411-445, 2007.

A. Saabas and T. Uustalu, “A compositional natural semantics and Hoare logic for low-level languages”, Theoretical Computer Science, Vol.373, No.1, pp.151-168, 2007.

V. Vafeiadis, “Concurrent separation logic and operational semantics”, Electronic Notes in Theoretical Computer Science, Vol.276, No.1, pp.335-351, 2011.

F. Besson, T. Jensen and D. Pichardie, “Proof-carrying code from certified abstract interpretation and fixpoint compression”, Theoretical Computer Science, Vol.364, No.3, pp.273-291, 2006.

N. Shavit and T. Dan, “Software transactional memory”, Distributed Computing, Vol.10, No.2, pp.99-116, 1997.

J. Larus and C. Kozyrakis, “Transactional memory”, Communications of the ACM, Vol.51, No.7, pp.80-88, 2007.

H.A. Lopez, E.R.B. Marques, F. Martins, et al., “Protocolbased verification of message-passing parallel programs”, ACM SIGPLAN Notices, Vol.50, No.10, pp.280-298, 2015.

M. Fu, Y. Zhang and Y. Li, “Formal reasoning about concurrent assembly code with reentrant locks”, IEEE International Symposium on Theoretical Aspects of Software Engineering, IEEE, Tianjin, China, pp.233-240, 2009.

Y. Zhu, L. Zhang, S. Wang, et al., “Verifying parallel low-level programs for multi-core processor”, Acta Electronica Sinica, Vol.37, No.S1, pp.1-6, 2009. (in Chinese)

Relative Articles

Supplements(0)

Cited By

Proportional views