Verification of Operating System Exception Management for SPARC Processor Architecture

被引：0
|
作者：
Ma Z. [1 ]
Qiao L. [1 ,3 ]
Yang M.-F. [2 ]
Li S.-F. [1 ,4 ]
机构：
[1] Beijing Institute of Control Engineering, Beijing
[2] China Academy of Space Technology, Beijing
[3] State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing
[4] School of Computer Science and Technology, Xidian University, Xi'an
来源：
Ruan Jian Xue Bao/Journal of Software | 2021年 / 32卷 / 06期
基金：
中国国家自然科学基金;
关键词：
Exception management; Exception nesting; Formal verification; Operating system; Task switching;
D O I：
10.13328/j.cnki.jos.006241
中图分类号：
学科分类号：
摘要：
Safety-critical systems such as spacecraft are typical embedded systems with the characteristics of multi-task concurrency and frequent interruptions. The operating system is the most fundamental software of computer, and building a correct operating system is crucial to ensure the reliability of the spacecraft system. Exception management, as the lowest level function of the operating system, is responsible for guiding sudden changes of control flow in response to certain changes in the processor state. Exception management is the basis for the correctness of the entire operating system correctness. This study proposes a verification framework based on Hoare-logic to prove the correctness of exception management for SPARC processor architecture operating systems. Especially for multi-task concurrency and frequent interruption of real-time operating system exception nesting and task switching in exceptions, the exception management is divided into five stages for comprehensive formal modeling, and this framework is implemented in the Coq proving theorem assistant tool. Based on this framework, the correctness of the exception management function of the spacecraft embedded real- time operating system SpaceOS, which is actually used by China's Beidou-3, is verified. © Copyright 2021, Institute of Software, the Chinese Academy of Sciences. All rights reserved.
引用
收藏
页码：1631 / 1646
页数：15
相关论文
共 18 条
  • [1] Wang J, Zhan NJ, Feng XY, Liu ZM., Overview of formal methods, Ruan Jian Xue Bao/Journal of Software, 30, 1, pp. 33-61, (2019)
  • [2] Klein G, Elphinstone K, Heiser G, Andronick J, Cock D, Derrin P, Elkaduwe D, Engerlhardt K, Kolanski R, Norrish M, Sewell T., seL4: Formal verification of an OS kernel, Proc. of the ACM SIGOPS 22nd Symp. on Operating Systems Principles, pp. 207-220, (2009)
  • [3] Chen H, Wu XN, Shao Z, Lockerman J, Gu RH., Toward compositional verification of interruptible OS kernels and device drivers, Proc. of the 37th ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI 2016), pp. 431-447, (2016)
  • [4] Gu RH, Shao Z, Chen H, Wu XN, Kim J, Sjoberg V, Costanzo D., CertiKOS: An extensible architecture for building certified concurrent OS kernels, Proc. of the 12th USENIX Conf. on Operating Systems Design and Implementation (OSDI 2016), pp. 653-669, (2016)
  • [5] Feng XY, Shao Z, Dong Y, Guo Y., Certifying low-level programs with hardware interrupts and preemptive threads, Proc. of the 29th ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI 2008), pp. 170-182, (2008)
  • [6] Feng XF, Shao Z, Guo Y, Dong Y., Combining domain-specific and foundational logics to verify complete software systems, Proc. of the VSTTE 2008, pp. 54-69, (2008)
  • [7] Qiao L, Yang MF, Tan YL, Pu GG, Yang H., Formal verification of memory management system in spacecraft using Event-B, Ruan Jian Xue Bao/Journal of Software, 28, 5, pp. 1204-1220, (2017)
  • [8] Jiang JJ, Qiao L, Yang MF, Yang H, Liu B., Operating system task management requirements layer modeling and verification based on Coq, Ruan Jian Xue Bao/Journal of Software, 31, 8, pp. 2375-2387, (2020)
  • [9] Regehr J, Cooprider N., Interrupt verification via thread verification, Electronic Notes in Theoretical Computer Science, 174, 9, pp. 139-150, (2007)
  • [10] Cui J, Duan ZH, Tian C, Zhang N., Modeling and analysis of nested interrupt systems, Ruan Jian Xue Bao/Journal of Software, 29, 6, pp. 1670-1680, (2018)
12