OTN保护倒换系统形式化建模及验证

目录

声明

1 绪论

1.1 课题研究背景和意义

1.2 国内外研究现状

1.3 模型验证基本原理

1.4 本文主要工作

1.5 本文组织结构

2 基于状态迁移表格的形式化建模方法

2.1 系统需求传统建模存在的问题

2.2 状态迁移表格基本结构

2.3 状态变迁表格形式化定义

2.4 状态迁移表格的动态行为描述

2.5 性质描述方法

2.6 本章小结

3 OTN保护倒换系统的STF模型及验证方法

3.1 OTN保护倒换系统及其STF模型

3.2 边界模型检测

3.3 STF模型的迁移规则

3.4 迁移规则的符号化编码

3.5 OTN保护倒换系统STF模型约束

3.6 本章小结

4 基于STF的等价类合并与模型验证方法

4.1 有限状态自动机形式化定义

4.2 有限状态自动机符号化编码方法

4.3 有限状态自动机压缩方法

4.4 基于STF的等价类合并方法

4.5 合并等价类后的STF验证

4.6 本章小结

5 实验与验证结果分析

5.1 实验环境与相关软件工具

5.2 OTN告警保护倒换系统的验证结果

5.3 嵌入式自动机模型验证结果

结论

参考文献

致谢