主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公English
2022年专刊出版计划 微信服务介绍 最新一期:2021年第2期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
马智,乔磊,杨孟飞,李少峰.面向SPARC处理器架构的操作系统异常管理形式化验证.软件学报,2021,32(6):16-0
面向SPARC处理器架构的操作系统异常管理形式化验证
Formal Verification of Operating System Exception Management for SPARC Processor Architecture
投稿时间:2020-08-17  修订日期:2020-10-26
DOI:10.13328/j.cnki.jos.006241
中文关键词:  操作系统  异常管理  异常嵌套  任务切换  形式化验证
英文关键词:Operating system  exception management  exception nesting  task switching  formal verification
基金项目:国家自然科学基金(61632005,61802017,62032004);中国科学院软件研究所计算机科学国家重点实验室开放课题(SYSKF1804)
作者单位E-mail
马智 北京控制工程研究所, 北京 100190  
乔磊 北京控制工程研究所, 北京 100190
计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190 
fly2moon@aliyun.com 
杨孟飞 中国空间技术研究院, 北京 100094  
李少峰 北京控制工程研究所, 北京 100190
西安电子科技大学 计算机科学与技术学院, 陕西 西安 710071 
 
摘要点击次数: 44
全文下载次数: 26
中文摘要:
      航天器等安全关键系统是典型的嵌入式系统,具有多任务并发、中断频发等特点,操作系统是其最基础的软件,构建一个正确的操作系统是保障航天器系统高可信运行的关键.异常管理作为操作系统最底层的功能负责引导系统控制流的突变来响应处理器状态中的某些变化,异常管理的正确性是整个操作系统正确性的基础.本文提出了一种基于Hoare-logic的验证框架,用于证明面向SPARC处理器架构操作系统异常管理的正确性,特别针对多任务并发和中断频发实时操作系统异常嵌套与异常中发生任务切换的情况,将异常管理划分为五个阶段进行全面的形式化建模,并且在Coq证明定理辅助工具中实现了此框架.基于该框架验证了我国北斗三号在轨实际应用的航天器嵌入式实时操作系统SpaceOS异常管理功能的正确性.
英文摘要:
      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 paper 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 our country's Beidou-3, is verified.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利