列车通信网络系统形式化建模与验证方法研究
| 摘要 | 第1-7页 |
| Abstract | 第7-15页 |
| 第1章 绪论 | 第15-31页 |
| ·研究背景及意义 | 第15-16页 |
| ·研究现状 | 第16-27页 |
| ·形式化建模 | 第16-21页 |
| ·形式化验证 | 第21-25页 |
| ·模拟验证 | 第25-27页 |
| ·列车通信网络系统建模与验证方法研究的必要性 | 第27-28页 |
| ·论文的主要工作 | 第28页 |
| ·论文的组织结构 | 第28-31页 |
| 第2章 列车通信网络系统与建模方法 | 第31-43页 |
| ·TCN协议分析 | 第31-37页 |
| ·WTB通信协议 | 第32-34页 |
| ·MVB通信协议 | 第34-36页 |
| ·WTB与MVB总线网关 | 第36-37页 |
| ·层次实时有色Petri网 | 第37-42页 |
| ·Petri网的基本原理 | 第38-39页 |
| ·层次实时有色Petri网 | 第39-42页 |
| ·本章小结 | 第42-43页 |
| 第3章 列车通信网络系统的静态属性分析 | 第43-63页 |
| ·引言 | 第43页 |
| ·相关工作 | 第43-44页 |
| ·列车通信网络系统建模 | 第44-55页 |
| ·网络拓扑结构建模 | 第44-49页 |
| ·链路层设备建模 | 第49-55页 |
| ·列车通信网络系统模型的静态属性 | 第55-62页 |
| ·拓扑有效性 | 第55-57页 |
| ·结构完整性 | 第57页 |
| ·功能确定性 | 第57-58页 |
| ·结构有界性 | 第58页 |
| ·行为实时性 | 第58-62页 |
| ·本章小结 | 第62-63页 |
| 第4章 列车通信网络系统的动态属性验证 | 第63-94页 |
| ·引言 | 第63页 |
| ·相关工作 | 第63-64页 |
| ·基于符号模型检查的验证方法 | 第64-71页 |
| ·Kripke结构 | 第64-65页 |
| ·NuSMV | 第65-66页 |
| ·属性描述与分类 | 第66-68页 |
| ·HRTCPN到NuSMV的语义转换 | 第68-71页 |
| ·基于时间自动机的验证方法 | 第71-73页 |
| ·时间自动机 | 第71-72页 |
| ·属性描述 | 第72页 |
| ·HRTCPN到时间自动机的语义转换 | 第72-73页 |
| ·列车通信网络系统的动态属性验证 | 第73-89页 |
| ·基于假设/保证的验证方法 | 第73-75页 |
| ·网络功能节点验证 | 第75-82页 |
| ·通信网络系统验证 | 第82-89页 |
| ·实验结果 | 第89-92页 |
| ·验证资源开销 | 第89-90页 |
| ·设计缺陷分析 | 第90-91页 |
| ·验证方法评价 | 第91-92页 |
| ·动态属性覆盖度量 | 第92页 |
| ·本章小结 | 第92-94页 |
| 第5章 列车通信网络控制器的模拟验证 | 第94-117页 |
| ·引言 | 第94-98页 |
| ·高级验证方法学 | 第95-96页 |
| ·验证策略与验证流程 | 第96-98页 |
| ·相关工作 | 第98-99页 |
| ·TCN控制器的功能验证 | 第99-110页 |
| ·基于SVA的断言验证 | 第99-100页 |
| ·模块级功能验证 | 第100-101页 |
| ·系统级功能验证 | 第101-103页 |
| ·网络拓扑级功能验证 | 第103-105页 |
| ·覆盖率驱动测试生成 | 第105-108页 |
| ·错误注入机制 | 第108-110页 |
| ·TCN控制器的综合后验证 | 第110-111页 |
| ·静态时序分析 | 第110页 |
| ·时序仿真 | 第110页 |
| ·基于FPGA的原型系统验证 | 第110-111页 |
| ·验证结果分析 | 第111-116页 |
| ·设计与规范的冲突 | 第111-112页 |
| ·异常处理与保护机制 | 第112页 |
| ·未定义的系统行为 | 第112页 |
| ·编码风格问题 | 第112页 |
| ·覆盖率统计分析 | 第112-114页 |
| ·各类验证信息汇总 | 第114-116页 |
| ·本章小结 | 第116-117页 |
| 结论 | 第117-119页 |
| 参考文献 | 第119-130页 |
| 攻读博士学位期间发表的论文和取得的科研成果 | 第130-132页 |
| 致谢 | 第132页 |
