文摘
英文文摘
第一章绪论
1.1论文选题的来源及意义
1.1.1 RT-Z的提出
1.1.2 RT-Z
1.1.3 RT-Z的特征
1.2国内外相关工作
1.2.1 CSP-OZ
1.2.2 TCOZ
1.2.3 Object-Z/CSP
1.2.4 LOTOS
1.2.5 RSL
1.3本课题的研究内容
第二章实时系统
2.1实时系统概述
2.1.1概念
2.1.2典型的实时系统
2.2实时系统的分类
2.2.1根据时间限制的程度分类
2.2.2按使用方式分类
2.3实时系统软件的特征
2.4实时系统的开发
2.4.1系统开发过程
2.4.2实时系统的需求分析
2.4.3实时系统的设计
2.4.4非形式设计方法
2.5实时系统的形式验证
第三章形式方法
3.1形式方法的定义
3.2主要内容
3.2.1形式规格说明
3.2.2形式验证
3.3形式方法的分类
3.3.1根据形式程度分类
3.3.2根据功能性质分类
3.3.3根据表达能力分类
3.3.4常见的顺序和并发程序形式方法
3.4形式方法在实时系统软件开发中的作用
3.4.1形式规格说明的作用
3.4.2定量证明的作用
3.4.3形式验证的作用
3.5形式方法在实时系统开发中的优点和局限性
3.5.1优点
3.5.2局限性
3.6形式方法的发展
3.6.1非形式方法和形式方法的结合
3.6.2面向对象方法与形式方法的结合
3.7形式化背景中的视点
第四章Z语言及其面向对象扩展
4.1 Z语言
4.1.1 Z模式
4.1.2 Z模式中常用符号
4.1.3 Z规格说明
4.1.4 Z语言的特点
4.1.5结构化Z规格说明
4.2 Z的面向对象扩展
4.2.1 Object-Z
4.2.2实时Object-Z
4.2.3Z++
4.2.4 Z++a
4.2.5 MOOZ
4.2.6 OOZE(object-oriented Z environment)
4.2.7 OOZS(object-oriented Z specification)
4.2.8 COOZ(Complete Object-Oriented Z)
4.2.9 GOOZ
第五章Z的实时扩展
5.1 TIMED CSP
5.1.1 CSP简介
5.1.2timed CSP
5.1.3实时失败模型
5.1.4实时失败语义
5.1.5规格说明宏
5.1.6timed CSP的优缺点
5.1.7 Timed CSP在实时系统开发中的应用
5.2 Z的扩展语言与UNTIMED/TIMED CSP的集成
5.2.1 CSP-OZ
5.2.2 TCOZ
5.2.3 Object-Z/CSP
5.3其它相关的形式化语言
5.3.1 LOTOS
5.3.2 RSL
5.3.3 TLA
5.4 RT-Z
5.4.1 Z和timed CSP集成可行性分析
5.4.2 RT-Z
5.4.3 RT-Z规格说明
5.4.4链接
5.4.5主要原则
5.4.6规格说明单元
5.4.7结构机制
5.4.8抽象规格说明单元(ASU)
5.4.9重命名
5.4.10隐藏
5.4.11参数化
5.4.12实例
第六章RT-Z的语义建立
6.1基础
6.2开放式系统观点的CSU
6.2.1一般数据状态的并发性
6.2.2语义集成概述
6.2.3历史模型
6.2.4扩展实时失败模型(ETFM)
6.2.5谓词语言
6.2.6 TFSM
6.2.7语义集成
6.3 ASU(开放系统观点)
6.4封闭系统观点
6.4.1 CSU
6.4.2 ASU
第七章与相关的集成形式方法的比较
7.1 CSP-OZ
7.1.1 CSP-OZ和RT-Z显著区别
7.1.2结论
7.2 TCOZ
7.2.1 TCOZ和RT-Z两个主要不同之处
7.2.2几个方面分析
7.3 OBJECT-Z/CSP
7.4 LOTOS
第八章RT-Z的实例研究—电梯系统
8.1问题描述和系统体系结构
8.2需求规格说明
8.3设计规格说明
8.4总结
结论
攻读硕士学位期间发表的论文
独创性声明
致谢
参考文献
