Page 57 - 《软件学报》2021年第6期

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
Journal of Software,2021,32(6):1631−1646 [doi: 10.13328/j.cnki.jos.006241] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563

∗
面向 SPARC 处理器架构的操作系统异常管理验证

1,3
1
2
马 智 , 乔 磊 , 杨孟飞 , 李少峰 1,4
1
(北京控制工程研究所,北京 100190)
2 (中国空间技术研究院,北京 100094)
3 (计算机科学国家重点实验室(中国科学院 软件研究所),北京 100190)
4
(西安电子科技大学 计算机科学与技术学院,陕西 西安 710071)
通讯作者: 乔磊, E-mail: fly2moon@aliyun.com

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

中文引用格式: 马智,乔磊,杨孟飞,李少峰.面向 SPARC 处理器架构的操作系统异常管理验证.软件学报,2021,32(6):
1631−1646. http://www.jos.org.cn/1000-9825/6241.htm
英文引用格式: Ma Z, Qiao L, Yang MF, Li SF. Verification of operating system exception management for SPARC processor
architecture. Ruan Jian Xue Bao/Journal of Software, 2021,32(6):1631−1646 (in Chinese). http://www.jos.org.cn/1000-9825/
6241.htm

Verification of Operating System Exception Management for SPARC Processor Architecture
1
1,3
2
MA Zhi , QIAO Lei , YANG Meng-Fei , LI Shao-Feng 1,4
1
(Beijing Institute of Control Engineering, Beijing 100190, China)
2
(China Academy of Space Technology, Beijing 100094, China)
3
(State Key Laboratory of Computer Science (Institute of Software, Chinese Academy of Sciences), Beijing 100190, China)
4
(School of Computer Science and Technology, Xidian University, Xi’an 710071, China)
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

∗ 基金项目: 国家自然科学基金(61632005, 61802017, 62032004); 中国科学院软件研究所计算机科学国家重点实验室开放课题
(SYSKF1804)
Foundation item: 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)
本文由“形式化方法与应用”专题特约编辑田聪教授推荐.
收稿时间: 2020-08-17; 修改时间: 2020-10-26; 采用时间: 2020-12-19; jos 在线出版时间: 2021-02-07