| 摘要 | 第1-3页 |
| Abstract | 第3-5页 |
| 目录 | 第5-10页 |
| 第一章 绪论 | 第10-14页 |
| ·课题的来源及意义 | 第10-11页 |
| ·形式描述技术(FDT)的提出 | 第10页 |
| ·形式描述技术(FDT)的概念 | 第10-11页 |
| ·形式描述技术(FDT)的特征 | 第11页 |
| ·国内外相关的工作 | 第11-13页 |
| ·本课题的研究内容 | 第13-14页 |
| 第二章 传统LOTOS介绍 | 第14-39页 |
| ·引言 | 第14-15页 |
| ·LOTOS的发展背景及过程 | 第14页 |
| ·LOTOS的技术基础 | 第14页 |
| ·LOTOS的语言特点 | 第14-15页 |
| ·LOTOS的语法介绍 | 第15-17页 |
| ·LOTOS的描述机制 | 第15-17页 |
| ·LOTOS描述进程的语法格式 | 第17页 |
| ·Basic LOTOS的行为表示 | 第17-23页 |
| ·不活动 | 第19页 |
| ·动作前缀(Action prefix) | 第19页 |
| ·选择(Choice) | 第19-20页 |
| ·循环 | 第20页 |
| ·并行操作器 | 第20-22页 |
| ·隐藏操作器(hiding) | 第22页 |
| ·使能操作器(enabling) | 第22-23页 |
| ·中止操作符(disabing) | 第23页 |
| ·LOTOS的数据类型 | 第23-29页 |
| ·介绍 | 第23-24页 |
| ·LOTOS的数据类型的概念 | 第24-29页 |
| ·FULL LOTOS | 第29-39页 |
| ·介绍 | 第29-30页 |
| ·结构化事件 | 第30-32页 |
| ·条件结构 | 第32-33页 |
| ·广义选择和并行表示 | 第33-34页 |
| ·带参数的进程(Parametric processes) | 第34-35页 |
| ·带值传递的序列组 | 第35-39页 |
| 第三章 形式描述技术LOTOS的实时扩展 | 第39-44页 |
| ·实时系统的介绍 | 第39-41页 |
| ·介绍 | 第39页 |
| ·实时系统的特征 | 第39-40页 |
| ·实时系统设计的要求 | 第40页 |
| ·实时系统的设计方法 | 第40-41页 |
| ·实时系统形式化的设计方法 | 第41页 |
| ·基于实时系统设计要求的形式技术的扩展 | 第41-42页 |
| ·形式技术的缺点 | 第41页 |
| ·形式技术的发展 | 第41-42页 |
| ·传统LOTOS的实时扩展 | 第42-44页 |
| ·传统LOTOS的不足 | 第42页 |
| ·传统LOTOS的时间扩展 | 第42-44页 |
| 第四章 TLOTOS | 第44-56页 |
| ·TLOTOS的介绍 | 第44页 |
| ·TLOTOS的实时扩展 | 第44-48页 |
| ·TLOTOS向上兼容性 | 第44-45页 |
| ·时控动作x的引入 | 第45页 |
| ·TLOTOS的扩展操作器 | 第45-48页 |
| ·TLOTOS的操作语义 | 第48-53页 |
| ·时控扩展的可能语义 | 第48-50页 |
| ·TLOTOS的操作语义 | 第50-53页 |
| ·TLOTOS的应用 | 第53-55页 |
| ·小结 | 第55-56页 |
| 第五章 ET-LOTOS | 第56-62页 |
| ·ET-LOTOS的介绍 | 第56页 |
| ·ET-LOTOS的实时扩展 | 第56-58页 |
| ·Timed LOTOS基本特征 | 第56-57页 |
| ·Timed LOTOS的缺点 | 第57-58页 |
| ·ET-LOTOS操作器的扩展 | 第58-59页 |
| ·数据类型和时间域 | 第58页 |
| ·前缀 | 第58页 |
| ·延迟 | 第58-59页 |
| ·ET-LOTOS的语义 | 第59-61页 |
| ·小结 | 第61-62页 |
| 第六章 RT-LOTOS | 第62-74页 |
| ·RT-LOTOS的介绍 | 第62页 |
| ·RT-LOTOS的扩展 | 第62-65页 |
| ·RT-LOTOS的时间约束行为 | 第62-65页 |
| ·RT-LOTOS的时间相关功能 | 第65页 |
| ·Basic RT-LOTOS的形式定义 | 第65-69页 |
| ·Basic RT-LOTOS形式语法 | 第65页 |
| ·操作语义 | 第65-66页 |
| ·基本属性 | 第66-68页 |
| ·行为等价和属性 | 第68-69页 |
| ·FULL RT-LOTOS的定义 | 第69-70页 |
| ·形式语法 | 第70页 |
| ·操作语义 | 第70页 |
| ·Basic RT-LOTOS~+的定义 | 第70-72页 |
| ·形式语法 | 第71-72页 |
| ·操作语义 | 第72页 |
| ·RT-LOTOS和ET-LOTOS的比较 | 第72-74页 |
| 第七章 E-LOTOS | 第74-108页 |
| ·介绍 | 第74-76页 |
| ·一个小例子--双通道寄存器 | 第74-75页 |
| ·变量 | 第75页 |
| ·E-LOTOS的时间 | 第75-76页 |
| ·E-LOTOS的扩展操作器 | 第76-89页 |
| ·动作 | 第76-77页 |
| ·顺序组合 | 第77-78页 |
| ·成功终端 | 第78页 |
| ·不活动和时间阻塞 | 第78页 |
| ·并行组合操作 | 第78-79页 |
| ·一般并行操作 | 第79-81页 |
| ·带值并行操作 | 第81页 |
| ·挂起／恢复恢复操作 | 第81-82页 |
| ·隐藏操作 | 第82-83页 |
| ·异常和异常处理 | 第83-84页 |
| ·等待延迟操作 | 第84-85页 |
| ·重命名名操作 | 第85-86页 |
| ·条件操作 | 第86页 |
| ·递归操作 | 第86-88页 |
| ·进程声明和实例化 | 第88-89页 |
| ·数据类型的基础语言 | 第89-100页 |
| ·数据类型 | 第89-92页 |
| ·类型表达式 | 第92-93页 |
| ·子类型 | 第93-94页 |
| ·表达式 | 第94-97页 |
| ·函数声明和实例化 | 第97-98页 |
| ·模式和模式匹配 | 第98-100页 |
| ·模块语言 | 第100-106页 |
| ·接口 | 第100-102页 |
| ·模块 | 第102-104页 |
| ·类属模块 | 第104-105页 |
| ·描述声明 | 第105-106页 |
| ·小结 | 第106-108页 |
| 第八章 形式描述技术的实例应用--分布式多媒体系统 | 第108-117页 |
| ·分布式多媒体系统的特征 | 第108页 |
| ·分布式多媒体系统分析 | 第108-110页 |
| ·分布式多媒体系统的形式化描述 | 第110-115页 |
| ·小结 | 第115-117页 |
| 结论 | 第117-119页 |
| 参考文献 | 第119-123页 |
| 攻读硕士学位期间发表的论文 | 第123-124页 |
| 致谢 | 第124-125页 |