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

Safety Mechanism Design and Verification of Safety Computer Parallel Program

doi: 10.1049/cje.2018.02.016
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
  • 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.
  • loading
  • 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)
  • 加载中


    通讯作者: 陈斌, bchen63@163.com
    • 1. 

      沈阳化工大学材料科学与工程学院 沈阳 110142

    1. 本站搜索
    2. 百度学术搜索
    3. 万方数据库搜索
    4. CNKI搜索

    Article Metrics

    Article views (312) PDF downloads(199) Cited by()
    Proportional views


    DownLoad:  Full-Size Img  PowerPoint