| 第一章 形式化方法 | 第1-16页 |
| §1．1 形式化方法概述 | 第11-13页 |
| §1．1．1 形式化方法基本概述 | 第11页 |
| §1．1．2 形式化方法的使用 | 第11-12页 |
| §1．1．3 形式化方法发展 | 第12-13页 |
| §1．1．4 与形式化方法相关的若干个术语 | 第13页 |
| §1．2 形式化方法研究内容 | 第13-14页 |
| §1．2．1 形式规约 | 第13-14页 |
| §1．2．2 形式验证 | 第14页 |
| §1．3 形式化方法的集成 | 第14-15页 |
| §1．4 本文的结构 | 第15-16页 |
| 第二章 B方法 | 第16-28页 |
| §2．1 B的历史 | 第16页 |
| §2．2 B方法简介 | 第16-17页 |
| §2．3 B方法的基础 | 第17-19页 |
| §2．3．1 谓词 | 第17页 |
| §2．3．2 表达式 | 第17-18页 |
| §2．3．3 组件 | 第18-19页 |
| §2．4 抽象机 | 第19-22页 |
| §2．5 精化和实现 | 第22-26页 |
| §2．6 B方法优越性 | 第26-28页 |
| 第三章 时间PETRI网 | 第28-39页 |
| §3．1 PETRI网的历史 | 第28-29页 |
| §3．2 网 | 第29-32页 |
| §3．2．1 基本概念 | 第29-30页 |
| §3．2．2 网系统 | 第30-31页 |
| §3．2．3 网系统的分类 | 第31-32页 |
| §3．3 P／T网 | 第32-35页 |
| §3．3．1 P／T网基本定义 | 第32-33页 |
| §3．3．2 P／T网的代数表示 | 第33页 |
| §3．3．3 P／T网的可达图 | 第33-35页 |
| §3．3．4 P／T网的活性 | 第35页 |
| §3．4 时间PETRI网 | 第35-37页 |
| §3．4．1 FIRING DURATION | 第36页 |
| §3．4．2 HOLDING DURATION | 第36-37页 |
| §3．4．3 ENABLING DURATION | 第37页 |
| §3．5 时间PETRI网定义 | 第37-39页 |
| 第四章 TPN和B方法的结合 | 第39-53页 |
| §4．1 结合的原因 | 第39-40页 |
| §4．2 TB网 | 第40-46页 |
| §4．2．1 TB网的定义 | 第40-42页 |
| §4．2．2 动态语义 | 第42-43页 |
| §4．2．3 TB网的特点 | 第43-46页 |
| §4．2．3．1 TB网主要特点 | 第43-44页 |
| §4．2．3．2 系统的状态 | 第44页 |
| §4．2．3．3 状态的转换 | 第44-45页 |
| §4．2．3．4 TB网的变量 | 第45-46页 |
| §4．3 TB网的构造 | 第46-52页 |
| §4．3．1 初始构造 | 第46-47页 |
| §4．3．2 TB网的改造 | 第47-52页 |
| §4．3．2．1 网改进的规则 | 第47-50页 |
| §4．3．2．2 TB网改进的规则 | 第50-52页 |
| §4．4 总结 | 第52-53页 |
| 第五章 TB网的若干性质 | 第53-81页 |
| §5．1 TB网的性质概述 | 第53页 |
| §5．2 用TB网描述ALTERNATING BIT PROTOCOL | 第53-80页 |
| §5．2．1 ALTERNATING BIT PROTOCOL协议介绍 | 第53-54页 |
| §5．2．2 用TB网构造初始ALTERNATING BIT PROTOCOL | 第54-61页 |
| §5．2．3 对初始TB网的改造 | 第61-70页 |
| §5．2．4 对TB网性质的讨论 | 第70-80页 |
| §5．2．4．1 对TB网可达性的讨论 | 第70-76页 |
| §5．2．4．2 对TB网时间约束的讨论 | 第76-79页 |
| §5．2．4．3 对TB网活性和有界性讨论 | 第79-80页 |
| §5．3 总结 | 第80-81页 |
| 第六章 总结与展望 | 第81-83页 |
| §6．1 总结 | 第81页 |
| §6．2 展望 | 第81-83页 |
| TB网工具 | 第83-97页 |
| 参考文献 | 第97-99页 |
| 致谢 | 第99页 |
