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

作     者：马智 乔磊 杨孟飞 李少峰 MA Zhi;QIAO Lei;YANG Meng-Fei;LI Shao-Feng

作者机构：北京控制工程研究所北京100190 中国空间技术研究院北京100094 计算机科学国家重点实验室(中国科学院软件研究所)北京100190 西安电子科技大学计算机科学与技术学院陕西西安710071 

出 版 物：《软件学报》 (Journal of Software)

年 卷 期：2021年第32卷第6期

页      面：1631-1646页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

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

主　　题：操作系统 异常管理 异常嵌套 任务切换 形式化验证 

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