中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
基于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实时操作系统所采用的三机冗余容错机制的正确性.
英文摘要: Computers have been increasingly used in recent years, along with which accidents due to software failures occur frequently. A solution to the software reliability problem is to use formal methods. Formal methods are techniques based on mathematics, such as logic, automata, algebra, and have been gradually applied to specify and verify software systems because of their precision and rigor. XYZ System consists of a Temporal Logic Language (TLL) XYZ/E to serve as its kernel and a kit of software engineering tools. The TLL XYZ/E is a programming language as well as a logic system, and can represent specification of different abstraction levels under a unified temporal logic framework. Since XYZ System is a progranirning support system with the goal to enhance reliability and productivity of software development, applying it to industrial use in solving practical problems, is of paramount significance. SZRTOS is a real-time operating system developed by the Aerospace Industry Ministry to support aeronautic applications. It has been written in assembly language and is a practical system whose reliability is highly required. In this thesis, the SZRTOS kernel is reconstructed in a stepwise refinement method of XYZ/E. Two topics concerning with the kernel, the correctness of the priority inheritance algorithms and the specification and verification of fault-tolerant systems, are also discussed. The accomplishment of the kernel-reconstruction work shows the feasability and effectiveness of applying XYZ System to develop high reliability software systems. The major contribution of this thesis is as follows: Firstly, the SZRTOS kernel is specified and implemented in a stepwise refinement method of XYZ/E, and the correctness of the kernel implementation is established through the verification of the semantics consistency between the two neighboring programs of each stepwise refinement procedure. During the verification process, some bugs in the kernel are also detected and fixed. Secondly, to remedy the defects in the original solution to the priority inversion problem, we propose a new algorithm to realize the basic priority inheritance protocol and prove its correctness. Thirdly, a model is put forward to specify the fault environment of XYZ/E executable programs. Based on the model, we study how to specify and verify fault-tolerant systems in XYZ/E. In addition, the correctness of the triple modular redundancy mechanism offered in the SZRTOS real-time operating system is also provided.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/5920
Appears in Collections:中科院软件所

Files in This Item:
File Name/ File Size Content Type Version Access License
LW008667.pdf(3619KB)----限制开放-- 联系获取全文

Recommended Citation:
郭亮. 基于XYZ/E重构SZRTOS实时操作系统内核[D]. 中国科学院软件研究所. 中国科学院软件研究所. 2002-01-01.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[郭亮]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[郭亮]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2017  中国科学院软件研究所 - Feedback
Powered by CSpace