| 题名 | 基于XYZ/E重构SZRTOS实时操作系统内核 |
| 作者 | 郭亮 |
| 学位类别 | 博士 |
| 答辩日期 | 2002 |
| 授予单位 | 中国科学院软件研究所 |
| 授予地点 | 中国科学院软件研究所 |
| 关键词 | 线性时序逻辑语言XYZ/E 逐步求精 优先级继承 容错系统 验证 |
| 其他题名 | Reconstructing the Kernel of SZRTOS Real-Time" OS in XYZ/E |
| 学位专业 | 计算机软件与理论 |
| 中文摘要 | SZRTOS实时操作系统是航天部开发的一个为航天应用程序提供底层服务支持的操作系统平台.系统采用汇编语言编写,是一个真正运转的实际应用系统,其内核对可靠性的要求也是很高的.论文工作采用逐步求精的方法,基于XYZ/E重构了SZRTOS实时操作系统内核,并讨论了与内核相关的两个问题：（1）优先级继承算法的正确生;（2）容错系统的描述和验证.内核重构工作的完成则说明了将XYZ系统应用于开发高可靠性软件系统的可行性和有效性.论文主要贡献及创新点如下：1.基于XYZ/E描述了SZRTOS实时操作系统内核的规范,并从此规范出发采用逐步求精的方法得到算法可执行内核,然后通过证明求精过程中各步骤间相邻两个程序的语义一致性保证内核的正确性.此外,在证明过程中,我们发现了内核原有设计存在的错误并对其进行了修正.2.针对内核原有设计对于优先级逆转问题的错误处理,对原算法进行改进,提出了一种实现基本优先级继承协议的算法并证明了算法正确性.3.提出了一种用于刻画XYZ/E可执行程序的错误环境的数学模型,基于此模型对如何使用XYZ/E描述和验证容错系统进行了研究,并讨论了SZRTOS实时操作系统所采用的三机冗余容错机制的正确性. |
| 语种 | 中文 |
| 公开日期 | 2011-03-17 |
| 页码 | 117 |
| 内容类型 | 学位论文 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/5920]  |
| 专题 | 软件研究所_中科院软件所_中科院软件所 |
| 推荐引用方式 GB/T 7714 | 郭亮. 基于XYZ/E重构SZRTOS实时操作系统内核[D]. 中国科学院软件研究所. 中国科学院软件研究所. 2002. |
| 个性服务 |
| 查看访问统计 |
| 相关权益政策 |
| 暂无数据 |
| 收藏/分享 |
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论