面向SPARC处理器架构的操作系统异常管理验证
作者:
作者简介:

马智(1994-),男,博士生,主要研究领域为空间飞行器嵌入式系统,控制系统,总体技术.
杨孟飞(1962-),男,博士,研究员,博士生导师,CCF高级会员,主要研究领域为空间飞行器嵌入式系统,控制系统,总体技术.
乔磊(1982-),男,博士,研究员,CCF专业会员,主要研究领域为操作系统模型设计,存储系统,文件系统.
李少峰(1992-),男,博士生,主要研究领域为操作系统内存管理,文件系统.

通讯作者:

乔磊,fly2moon@aliyun.com

基金项目:

国家自然科学基金(61632005,61802017,62032004);中国科学院软件研究所计算机科学国家重点实验室开放课题(SYSKF1804)


Verification of Operating System Exception Management for SPARC Processor Architecture
Author:
Fund Project:

National Natural Science Foundation of China (61632005, 61802017, 62032004); Open project of State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences (SYSKF1804)

  • 摘要
  • | |
  • 访问统计
  • |
  • 参考文献 [25]
  • |
  • 相似文献 [20]
  • | | |
  • 文章评论
    摘要:

    航天器等安全关键系统是典型的嵌入式系统,具有多任务并发、中断频发等特点.操作系统是其最基础的软件,构建一个正确的操作系统是保障航天器系统高可信运行的关键.异常管理作为操作系统最底层的功能,负责引导系统控制流的突变来响应处理器状态中的某些变化,异常管理的正确性是整个操作系统正确性的基础.提出一种基于Hoare-logic的验证框架,用于证明面向SPARC处理器架构操作系统异常管理的正确性,特别针对多任务并发和中断频发实时操作系统异常嵌套与异常中发生任务切换的情况,将异常管理划分为5个阶段进行全面的形式化建模,并且在Coq证明定理辅助工具中实现了此框架.基于该框架,验证了我国北斗三号在轨实际应用的航天器嵌入式实时操作系统SpaceOS异常管理功能的正确性.

    Abstract:

    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.

    参考文献
    [1] Wang J, Zhan NJ, Feng XY, Liu ZM. Overview of formal methods. Ruan Jian Xue Bao/Journal of Software, 2019,30(1):33-61(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5652.htm[doi:10.13328/j.cnki.jos.005652]
    [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. In:Proc. of the ACM SIGOPS 22nd Symp. on Operating Systems Principles. 2009. 207-220.
    [3] Chen H, Wu XN, Shao Z, Lockerman J, Gu RH. Toward compositional verification of interruptible OS kernels and device drivers. In:Proc. of the 37th ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI 2016). New York:Association for Computing Machinery, 2016. 431-447.
    [4] Gu RH, Shao Z, Chen H, Wu XN, Kim J, Sjöberg V, Costanzo D. CertiKOS:An extensible architecture for building certified concurrent OS kernels. In:Proc. of the 12th USENIX Conf. on Operating Systems Design and Implementation (OSDI 2016). USENIX Association, 2016. 653-669.
    [5] Feng XY, Shao Z, Dong Y, Guo Y. Certifying low-level programs with hardware interrupts and preemptive threads. In:Proc. of the 29th ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI 2008). New York:Association for Computing Machinery, 2008. 170-182.
    [6] Feng XF, Shao Z, Guo Y, Dong Y. Combining domain-specific and foundational logics to verify complete software systems. In:Proc. of the VSTTE 2008. 2008. 54-69.
    [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, 2017,28(5):1204-1220(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5218.htm[doi:10.13328/j.cnki.jos.005218]
    [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, 2020,31(8):2375-2387(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5961.htm[doi:10.13328/j.cnki.jos.005961]
    [9] Regehr J, Cooprider N. Interrupt verification via thread verification. Electronic Notes in Theoretical Computer Science, 2007, 174(9):139-150.[doi:10.1016/j.entcs.2007.04.002]
    [10] Cui J, Duan ZH, Tian C, Zhang N. Modeling and analysis of nested interrupt systems. Ruan Jian Xue Bao/Journal of Software, 2018,29(6):1670-1680(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5472.htm[doi:10.13328/j.cnki.jos. 005472]
    [11] Liu H, Zhang H, Jiang Y, et al. iDola:Bridge modeling to verification and implementation of interrupt-driven systems. In:Proc. of the Theoretical Aspects of Software Engineering Conf. (TASE). IEEE, 2014. 193-200.[doi:10.1109/TASE.2014.33]
    [12] Alur R, Dill DL. A theory of timed automata. Theoretical Computer Science, 1994,126(2):183-235.
    [13] Zhou XY, Gu B, Zhao JH, Yang MF, Li XD. Model checking technique for interrupt-driven system. Ruan Jian Xue Bao/Journal of Software, 2015,26(9):2212-2230(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/4713.htm[doi:10.13328/j. cnki.jos.004713]
    [14] Najumudheen ESF, Mall R, Samanta D. Modeling and coverage analysis of programs with exception handling. In:Proc. of the 12th Innovations on Software Engineering Conf., Formerly Known as India Software Engineering Conf. (ISEC 2019). Article 15. New York:Association for Computing Machinery, 2019. 1-11.[doi:https://doi.org/10.1145/3299771.3299785]
    [15] Robillard MP, Murphy GC. Static analysis to support the evolution of exception structure in object-oriented systems. ACM Trans. on Softw. Eng. Methodol, 2003,12(2):191-221.[doi:https://doi.org/10.1145/941566.941569]
    [16] Harr R, Kaptelinin V. Interrupting or not:Exploring the effect of social context on interrupters' decision making. In:Proc. of the 7th Nordic Conf. on Human-Computer Interaction:Making Sense through Design (NordiCHI 2012). New York:Association for Computing Machinery, 2012. 707-710.[doi:https://doi.org/10.1145/2399016.2399124]
    [17] Sozeau M, Boulier S, Forster Y, Tabareau N, Winterhalter T. Coq Coq correct! Verification of type checking and erasure for Coq, in Coq. In:Proc. of the ACM Program. Lang. 4, POPL, Article 8. 2020. 28.[doi:https://doi.org/10.1145/3371076]
    [18] Yang YX, Xu YY, Li JL, Yang C. Progress and performance evaluation of Bei Dou global navigation satellite system:Data analysis based on BDS-3 demonstration system. Scientia Sinica (Terrae), 2018,48(5):584-594(in Chinese with English abstract).
    附中文参考文献:
    [1] 王戟,詹乃军,冯新宇,刘志明.形式化方法概貌.软件学报,2019,30(1):33-61. http://www.jos.org.cn/1000-9825/5652.htm[doi:10.13328/j.cnki.jos.005652]
    [7] 乔磊,杨孟飞,谭彦亮,蒲戈光,杨桦.基于Event-B的航天器内存管理系统形式化验证.软件学报,2017,28(5):1204-1220. http://www.jos.org.cn/1000-9825/5218.htm[doi:10.13328/j.cnki.jos.005218]
    [8] 姜菁菁,乔磊,杨孟飞,杨桦,刘波.基于Coq的操作系统任务管理需求层建模及验证.软件学报,2020,31(8):2375-2387. http://www.jos.org.cn/1000-9825/5961.htm[doi:10.13328/j.cnki.jos.005961]
    [10] 崔进,段振华,田聪,张南.一种嵌套中断系统的建模和分析方法.软件学报,2018,29(6):1670-1680. http://www.jos.org.cn/1000-9825/5472.htm[doi:10.13328/j.cnki.jos.005472]
    [13] 周筱羽,顾斌,赵建华,杨孟飞,李宣东.中断驱动系统模型检验.软件学报,2015,26(9):2212-2230. http://www.jos.org.cn/1000-9825/4713.htm[doi:10.13328/j.cnki.jos.004713]
    [18] 杨元喜,许扬胤,李金龙,杨诚.北斗三号系统进展及性能预测——实验验证数据分析.中国科学(地球科学),2018,48(5):584-594.
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

马智,乔磊,杨孟飞,李少峰.面向SPARC处理器架构的操作系统异常管理验证.软件学报,2021,32(6):1631-1646

复制
分享
文章指标
  • 点击次数:2099
  • 下载次数: 5530
  • HTML阅读次数: 3680
  • 引用次数: 0
历史
  • 收稿日期:2020-08-17
  • 最后修改日期:2020-10-26
  • 在线发布日期: 2021-02-07
  • 出版日期: 2021-06-06
文章二维码
您是第20474511位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号