| 摘要 | 第1-4页 |
| ABSTRACT | 第4-6页 |
| 目录 | 第6-11页 |
| 第一章 绪论 | 第11-19页 |
| 1．1 论文选题的来源及意义 | 第11-13页 |
| 1．1．1 RT-Z的提出 | 第11-12页 |
| 1．1．2 RT-Z | 第12页 |
| 1．1．3 RT-Z的特征 | 第12-13页 |
| 1．2 国内外相关工作 | 第13-17页 |
| 1．2．1 CSP-OZ | 第13-14页 |
| 1．2．2 TCOZ | 第14-15页 |
| 1．2．3 Object-Z/CSP | 第15-16页 |
| 1．2．4 LOTOS | 第16-17页 |
| 1．2．5 RSL | 第17页 |
| 1．3 本课题的研究内容 | 第17-19页 |
| 第二章 实时系统 | 第19-29页 |
| 2．1 实时系统概述 | 第19-20页 |
| 2．1．1 概念 | 第19-20页 |
| 2．1．2 典型的实时系统 | 第20页 |
| 2．2 实时系统的分类 | 第20-22页 |
| 2．2．1 根据时间限制的程度分类 | 第20页 |
| 2．2．2 按使用方式分类 | 第20-22页 |
| 2．3 实时系统软件的特征 | 第22-23页 |
| 2．4 实时系统的开发 | 第23-28页 |
| 2．4．1 系统开发过程 | 第23-24页 |
| 2．4．2 实时系统的需求分析 | 第24-26页 |
| 2．4．3 实时系统的设计 | 第26页 |
| 2．4．4 非形式设计方法 | 第26-28页 |
| 2．5 实时系统的形式验证 | 第28-29页 |
| 第三章 形式方法 | 第29-43页 |
| 3．1 形式方法的定义 | 第29页 |
| 3．2 主要内容 | 第29-31页 |
| 3．2．1 形式规格说明 | 第29-30页 |
| 3．2．2 形式验证 | 第30-31页 |
| 3．3 形式方法的分类 | 第31-33页 |
| 3．3．1 根据形式程度分类 | 第31页 |
| 3．3．2 根据功能性质分类 | 第31-32页 |
| 3．3．3 根据表达能力分类 | 第32页 |
| 3．3．4 常见的顺序和并发程序形式方法 | 第32-33页 |
| 3．4 形式方法在实时系统软件开发中的作用 | 第33-35页 |
| 3．4．1 形式规格说明的作用 | 第33-34页 |
| 3．4．2 定量证明的作用 | 第34页 |
| 3．4．3 形式验证的作用 | 第34-35页 |
| 3．5 形式方法在实时系统开发中的优点和局限性 | 第35-36页 |
| 3．5．1 优点 | 第35-36页 |
| 3．5．2 局限性 | 第36页 |
| 3．6 形式方法的发展 | 第36-41页 |
| 3．6．1 非形式方法和形式方法的结合 | 第37页 |
| 3．6．2 面向对象方法与形式方法的结合 | 第37-41页 |
| 3．7 形式化背景中的视点 | 第41-43页 |
| 第四章 Z语言及其面向对象扩展 | 第43-53页 |
| 4．1 Z语言 | 第43-48页 |
| 4．1．1 Z模式 | 第43页 |
| 4．1．2 Z模式中常用符号 | 第43-44页 |
| 4．1．3 Z规格说明 | 第44-46页 |
| 4．1．4 Z语言的特点 | 第46-47页 |
| 4．1．5 结构化Z规格说明 | 第47-48页 |
| 4．2 Z的面向对象扩展 | 第48-53页 |
| 4．2．1 Object-Z | 第49页 |
| 4．2．2 实时Object-2 | 第49-50页 |
| 4．2．3 Z~(++) | 第50页 |
| 4．2．4 Z~(++a) | 第50-51页 |
| 4．2．5 MOOZ | 第51页 |
| 4．2．6 OOZE(otiject-oriented Z environment) | 第51页 |
| 4．2．7 OOZS(object-oriented Z specification) | 第51页 |
| 4．2．8 COOZ(Complete Object-Oriented Z) | 第51-52页 |
| 4．2．9 GOOZ | 第52-53页 |
| 第五章 Z的实时扩展 | 第53-83页 |
| 5．1 TIMED CSP | 第53-61页 |
| 5．1．1 CSP简介 | 第53页 |
| 5．1．2 timed CSP | 第53-56页 |
| 5．1．3 实时失败模型 | 第56页 |
| 5．1．4 实时失败语义 | 第56-59页 |
| 5．1．5 规格说明宏 | 第59-60页 |
| 5．1．6 timed CSP的优缺点 | 第60页 |
| 5．1．7 Timed CSP在实时系统开发中的应用 | 第60-61页 |
| 5．2 Z的扩展语言与 UNTIMED/TIMED CSP的集成 | 第61-62页 |
| 5．2．1 CSP-OZ | 第61页 |
| 5．2．2 TCOZ | 第61-62页 |
| 5．2．3 Object-Z/CSP | 第62页 |
| 5．3 其它相关的形式化语言 | 第62-63页 |
| 5．3．1 LOTOS | 第62页 |
| 5．3．2 RSL | 第62-63页 |
| 5．3．3 TLA | 第63页 |
| 5．4 RT-Z | 第63-83页 |
| 5．4．1 Z和timed CSP集成可行性分析 | 第63-64页 |
| 5．4．2 RT-Z | 第64页 |
| 5．4．3 RT-Z规格说明 | 第64-65页 |
| 5．4．4 链接 | 第65-66页 |
| 5．4．5 主要原则 | 第66-68页 |
| 5．4．6 规格说明单元 | 第68-71页 |
| 5．4．7 结构机制 | 第71-78页 |
| 5．4．8 抽象规格说明单元(ASU) | 第78-80页 |
| 5．4．9 重命名 | 第80-81页 |
| 5．4．10 隐藏 | 第81页 |
| 5．4．11 参数化 | 第81页 |
| 5．4．12 实例 | 第81-83页 |
| 第六章 RT-Z的语义建立 | 第83-105页 |
| 6．1 基础 | 第83-84页 |
| 6．2 开放式系统观点的CSU | 第84-102页 |
| 6．2．1 一般数据状态的并发性 | 第84-85页 |
| 6．2．2 语义集成概述 | 第85-86页 |
| 6．2．3 历史模型 | 第86-94页 |
| 6．2．4 扩展实时失败模型(ETFM) | 第94-99页 |
| 6．2．5 谓词语言 | 第99-100页 |
| 6．2．6 TFSM | 第100-101页 |
| 6．2．7 语义集成 | 第101-102页 |
| 6．3 ASU(开放系统观点) | 第102-104页 |
| 6．4 封闭系统观点 | 第104-105页 |
| 6．4．1 CSU | 第104页 |
| 6．4．2 ASU | 第104-105页 |
| 第七章 与相关的集成形式方法的比较 | 第105-113页 |
| 7．1 CSP-OZ | 第105-108页 |
| 7．1．1 CSP-OZ和RT-Z显著区别 | 第105-107页 |
| 7．1．2 结论 | 第107-108页 |
| 7．2 TCOZ | 第108-111页 |
| 7．2．1 TCOZ和RT-Z两个主要不同之处 | 第108-109页 |
| 7．2．2 几个方面分析 | 第109-111页 |
| 7．3 OBJECT-Z/CSP | 第111页 |
| 7．4 LOTOS | 第111-113页 |
| 第八章 RT-Z的实例研究-电梯系统 | 第113-126页 |
| 8．1 问题描述和系统体系结构 | 第113-114页 |
| 8．2 需求规格说明 | 第114-117页 |
| 8．3 设计规格说明 | 第117-125页 |
| 8．4 总结 | 第125-126页 |
| 结论 | 第126-128页 |
| 攻读硕士学位期间发表的论文 | 第128-129页 |
| 独创性声明 | 第129-130页 |
| 致谢 | 第130-131页 |
| 参考文献 | 第131-134页 |
