We use cookies to improve your experience with our site.

Indexed in:

SCIE, EI, Scopus, INSPEC, DBLP, CSCD, etc.

Submission System
(Author / Reviewer / Editor)
Advanced Search
Volume 36 Issue 6
November  2021
Turn off MathJax
Article Contents
Abstract
References
Supplements
Zhi Ma, Lei Qiao, Meng-Fei Yang, Shao-Feng Li, Jin-Kun Zhang. Verification of Real Time Operating System Exception Management Based on SPARCv8[J]. Journal of Computer Science and Technology, 2021, 36(6): 1367-1387. DOI: 10.1007/s11390-021-1644-x
Citation: Zhi Ma, Lei Qiao, Meng-Fei Yang, Shao-Feng Li, Jin-Kun Zhang. Verification of Real Time Operating System Exception Management Based on SPARCv8[J]. Journal of Computer Science and Technology, 2021, 36(6): 1367-1387. DOI: 10.1007/s11390-021-1644-x
shu

Verification of Real Time Operating System Exception Management Based on SPARCv8

  • 1 Beijing Institute of Control Engineering, Beijing 100190, China;
    2 China Academy of Space Technology, Beijing 100094, China;
    3 School of Computer Science and Technology, Xidian University, Xi'an 710071, China

Funds: This work was supported by the National Natural Science Foundation of China under Grant Nos. 61632005 and 62032004.
More Information
  • Corresponding author:

    Lei Qiao E-mail: fly2moon@aliyun.com

  • Received Date: May 30, 2021
  • Revised Date: November 15, 2021
  • Published Date: November 29, 2021
    Abstract
  • Exception management, as the lowest level function module of the operating system, is responsible for making abrupt changes in the control flow to react to exception events in the system. The correctness of the exception management is crucial to guaranteeing the safety of the whole system. However, existing formal verification projects have not fully considered the issues of exceptions at the assembly level. Especially for real-time operating systems, in addition to basic exception handling, there are nested exceptions and task switching by exceptions service routine. In our previous work, we used high-level abstraction to describe the basic elements of the exception management and verified correctness only at the requirement layer. Building on earlier work, this paper proposes EMS (Exception Management SPARCv8), a practical Hoare-style program framework to verify the exception management based on SPARCv8 (Scalable Processor Architecture Version 8) at the design layer. The framework describes the low-level details of the machine, such as registers and memory stack. It divides the execution logic of the exception management into six phases for comprehensive formal modeling. Taking the executing scenario of the real-time operating system SpaceOS on the Beidou-3 satellite as an example, we use the EMS framework to verify the exception management. All the formalization and proofs are implemented in the interactive theorem prover Coq.
    • FullText(HTML)
    • References (24)
  • [1]
    Klein G, Elphinstone K, Heiser G, Andronick J, Cock D, Derrin P, Elkaduwe D, Engelhardt K, Kolanski R, Norrish M, Sewell T, Tuch H, Winwood S. seL4: Formal verification of an OS Kernel. In Proc. the 22nd ACM Symposium on Operating Systems Principles, Oct. 2009, pp.207-220. DOI: 10.1145/1629575.1629596.
    [2]
    Gu R H, Shao Z, Chen H, Wu X N, Kim J, Sjöberg V, Costanzo D. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In Proc. the 12th USENIX Conf. Operating Systems Design and Implementation, Nov. 2016, pp.653-669.
    [3]
    Chen H, Wu X N, Shao Z, Lockerman J, Gu R H. Toward compositional verification of interruptible OS kernels and device drivers. In Proc. the 37th ACM SIGPLAN Conf. Programming Language Design and Implementation, June 2016, pp.431-447. DOI: 10.1145/2908080.2908101.
    [4]
    Xu F, Fu M, Feng X, Zhang X, Zhang H, Li Z. A practical verification framework for preemptive OS kernels. In Proc. the 28th International Conference on Computer Aided Verification, July 2016, pp.59-79. DOI: 10.1007/978-3-319-41540-6-4.
    [5]
    Ma Z, Qiao L, Yang M F, Li S F. Verification of operating system exception management for SPARC processor architecture. Journal of Software, 2021, 32(6): 1631-1646. DOI: 10.13328/j.cnki.jos.006241. (in Chinese).
    [6]
    Maruyama T, Yoshida T, Kan R et al. Sparc64 VⅢfx: A new-generation octocore processor for petascale computing. IEEE Micro, 2010, 30(2): 30-40. DOI: 10.1109/MM.2010.40.
    [7]
    Qiao L, Yang M, Gu B, Yang H, Liu B. An embedded operating system design for the lunar exploration rover. In Proc. the 5th International Conference on Secure Software Integration and Reliability Improvement, June 2011, pp.160-165. DOI: 10.1109/SSIRI-C.2011.39.
    [8]
    Zha J P, Feng X Y, Qiao L. Modular verification of SPARCv8 code. Journal of Computer Science and Technology, 2020, 35(6): 1382-1405. DOI: 10.1007/s11390-020-0536-9.
    [9]
    Wang J, Fu M, Qiao L et al. Formalizing SPARCv8 instruction set architecture in Coq. Science of Computer Programming, 2019, 187: Article No. 102371. DOI: 10.1016/j.scico.2019.102371.
    [10]
    Hoare C A. An axiomatic basis for computer programming. Communications of the ACM, 1969, 12(10): 576-580. DOI: 10.1145/363235.363259.
    [11]
    Bryant R, O’Hallaron D. Computer Systems: A Programmer’s Perspective (3rd edition). Pearson, 2016.
    [12]
    Zapletal J, Merta M, Malý L. Boundary element quadrature schemes for multi-and many-core architectures. Computers and Mathematics with Applications, 2017, 74(1): 157-173. DOI: 10.1016/j.camwa.2017.01.018.
    [13]
    Fang J B, Liao X K, Huang C et al. Performance evaluation of memory-centric ARMv8 many-core architectures: A case study with Phytium 2000+. Journal of Computer Science and Technology, 2021, 36(1): 33-43. DOI: 10.1007/s11390-020-0741-6.
    [14]
    Patterson D A, Hennessy J L. Computer Organization and Design: The Hardware/Software Interface (ARM edition). Morgan Kaufmann, 2016.
    [15]
    Paulson L C. Isabelle: A Generic Theorem Prover. Springer, 1994. DOI: 10.1007/BFb0030541.
    [16]
    Bevier W R. Kit: A study in operating system verification. IEEE Trans. Softw. Eng., 1989, 15(11): 1382-1396. DOI: 10.1109/32.41331.
    [17]
    Gargano M, Hillebrand M A, Leinenbach D, Paul W J. On the correctness of operating system kernels. In Proc. the 18th International Conference on Theorem Proving in Higher Order Logics, August 2005, pp.1-16. DOI: 10.1007/11541868-1.
    [18]
    Ni Z, Yu D, Shao Z. Using XCAP to certify realistic systems code: Machine context management. In Proc. the 20th International Conference on Theorem Proving in Higher Order Logics, Sept. 2007, pp.189-206. DOI: 10.1007/978-3-540-74591-4-15.
    [19]
    Liu H, Zhang H, Jiang Y et al. iDola: Bridge modeling to verification and implementation of interrupt-driven systems. In Proc. the 2014 Theoretical Aspects of Software Engineering Conf., Sept. 2014, pp.193-200. DOI: 10.1109/TASE.2014.33.
    [20]
    Suenaga K, Kobayashi N. Type based analysis of deadlock for a concurrent calculus with interrupts. In Proc. the 16th European Symposium on Programming, March 24–April 1, 2007, pp.490-504. DOI: 10.1007/978-3-540-71316-6-33.
    [21]
    Duan J, Regehr J. Correctness proofs for device drivers in embedded systems. In Proc. the 5th International Conference on Systems Software Verification, Oct. 2010.
    [22]
    Fox A, Myreen M. A trustworthy monadic formalization of the ARMv7 instruction set architecture. In Proc. the 1st International Conference on Interactive Theorem Proving, July 2010, pp.243-258. DOI: 10.1007/978-3-642-14052-5-18.
    [23]
    Feng X, Shao Z, Vaynberg A, Xiang S, Ni Z. Modular verification of assembly code with stack-based control abstractions. In Proc. the 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2006, pp.401-414. DOI: 10.1145/1133981.1134028.
    [24]
    Kennedy A. Benton N, Jensen J B, Dagand P E. Coq: the world’s best macro assembler? In Proc. the 15th Symposium on Principles and Practice of Declarative Programming, Sept. 2013, pp.13-24. DOI: 10.1145/2505879.2505897.
    • Relative Articles
  • Supplements (2)

  • Others

  • Cited by

    Periodical cited type(4)

    1. Hongbiao Liu, Mengfei Yang, Lei Qiao, et al. An efficient schedulability analysis based on worst-case interference time for real-time systems. Science China Information Sciences, 2024, 67(9) DOI:10.1007/s11432-022-3891-4
    2. Hongbiao Liu, Mengfei Yang, Tingyu Wang, et al. A heuristic mixed real-time task allocation of virtual utilization in multi-core processor. Journal of Information and Intelligence, 2023, 1(2): 156. DOI:10.1016/j.jiixd.2023.03.002
    3. Mina Soltani Siapoush, Jim Alves-Foss. Is Formal Verification of seL4 Adequate to Address the Key Security Challenges of Kernel Design?. IEEE Access, 2023, 11: 101750. DOI:10.1109/ACCESS.2023.3316031
    4. Wang Zhao, Pengfei Xu, Li Zhou, et al. Debugging Method for Segmentation Faults Based on Hardware-Software Co-Analysis for Processor Verification. 2024 9th International Symposium on Computer and Information Processing Technology (ISCIPT), DOI:10.1109/ISCIPT61983.2024.10672771

    Other cited types(0)

Catalog

    Get Citation
    PDF
    XML
    Read Online
    Article views (66) PDF downloads (1) Cited by(4)
    Related

    Copyright ©2025 JCST, All Rights Reserved     京ICP备05002829号-1

    Institute of Computing Technology, Chinese Academy of Sciences
    P.O. Box 2704, Beijing 100190, P.R. China

    Tel.: 86-10-62610746 E-mail: jcst@ict.ac.cn

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return