软件学报

作者：马智，乔磊，杨孟飞，李少峰

单位：马智，北京控制工程研究所, 北京 10019011,乔磊，北京控制工程研究所, 北京 100190;计算机科学国家重点实验室(中国科学院 软件研究所), 北京 10019002,杨孟飞，中国空间技术研究院, 北京 10009403,李少峰，北京控制工程研究所, 北京 100190;西安电子科技大学 计算机科学与技术学院, 陕西 西安 71007104

关键词：操作系统;异常管理;异常嵌套;任务切换;形式化验证

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

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

来源：2021年第6期

《软件学报》期刊编辑部

查看软件学报杂志2021年第6期