| 摘要 | 第1-11页 |
| ABSTRACT | 第11-13页 |
| 第一章 绪论 | 第13-23页 |
| ·研究背景 | 第13-14页 |
| ·C~4ISR系统建设对体系结构设计的需求 | 第13页 |
| ·体系结构动态行为在C~4ISR体系结构设计中的地位 | 第13页 |
| ·本文研究问题的提出 | 第13-14页 |
| ·国内外研究现状 | 第14-21页 |
| ·体系结构动态行为建模 | 第14-17页 |
| ·系统模型的一致性问题 | 第17-18页 |
| ·体系结构验证技术 | 第18-21页 |
| ·本文主要工作和结构 | 第21-23页 |
| 第二章 C~4ISR体系结构动态行为一致性验证 | 第23-38页 |
| ·体系结构设计中的动态行为产品 | 第23-27页 |
| ·体系结构的动态行为和C~4ISR系统的动态特性 | 第23-24页 |
| ·动态行为产品及模型描述 | 第24-27页 |
| ·动态行为产品的关系分析 | 第27-32页 |
| ·动态行为产品之间的关系 | 第27-29页 |
| ·动态行为产品与其他产品的关系 | 第29-32页 |
| ·动态行为一致性验证的内容和基本过程 | 第32-37页 |
| ·动态行为关键产品的提出 | 第32-33页 |
| ·动态行为一致性验证内容的确立 | 第33-34页 |
| ·动态行为一致性验证的基本过程 | 第34-37页 |
| ·小结 | 第37-38页 |
| 第三章 基于形式化描述的动态行为语法一致性验证方法 | 第38-51页 |
| ·动态行为关键产品的形式化描述 | 第38-42页 |
| ·OV-6b和SV-10b的形式化描述 | 第38-40页 |
| ·OV6-c和SV10-c的形式化描述 | 第40-42页 |
| ·动态行为产品语法一致性规则 | 第42-45页 |
| ·作战视图动态行为关键产品的语法一致性规则 | 第42-44页 |
| ·系统视图动态行为关键产品的语法一致性规则 | 第44-45页 |
| ·动态行为语法一致性的验证方法 | 第45-50页 |
| ·节点一致的算法 | 第45-46页 |
| ·事件数目一致的算法 | 第46-47页 |
| ·事件引用一致的算法 | 第47-48页 |
| ·事件顺序一致的算法 | 第48-50页 |
| ·小结 | 第50-51页 |
| 第四章 基于对象Petri网的动态行为语义一致性验证方法 | 第51-73页 |
| ·动态行为产品语义一致性规则 | 第51-53页 |
| ·作战视图动态行为关键产品的语义一致性规则 | 第51-52页 |
| ·系统视图动态行为关键产品的语义一致性规则 | 第52-53页 |
| ·基于中间产品的可执行模型生成方法 | 第53-67页 |
| ·中间产品的提出 | 第53-55页 |
| ·建立和检查中间产品的方法 | 第55-58页 |
| ·对象Petri网的形式化描述及其XML规范 | 第58-62页 |
| ·中间产品转换为对象Petri网的方法 | 第62-67页 |
| ·利用OPMSE进行可执行验证 | 第67-72页 |
| ·对象Petri网的执行条件 | 第68页 |
| ·运行情况描述 | 第68-70页 |
| ·动态行为产品语义一致的判断 | 第70-72页 |
| ·小结 | 第72-73页 |
| 第五章 动态行为一致性验证原型系统实现及案例研究 | 第73-86页 |
| ·原型系统的总体设计 | 第73-74页 |
| ·原型系统总体设计目标 | 第73页 |
| ·原型系统总体结构 | 第73-74页 |
| ·原型系统的具体实现 | 第74-77页 |
| ·产品数据的表结构设计 | 第74-75页 |
| ·各功能模块的实现与接口 | 第75-77页 |
| ·案例研究 | 第77-85页 |
| ·某旅防空指挥信息系统概述 | 第77-78页 |
| ·某旅防空指挥信息系统体系结构描述 | 第78-80页 |
| ·某旅防空指挥信息系统体系结构动态行为一致性验证 | 第80-85页 |
| ·小结 | 第85-86页 |
| 第六章 结束语 | 第86-89页 |
| ·本文的主要贡献 | 第86-87页 |
| ·今后进一步的工作 | 第87-89页 |
| 致谢 | 第89-90页 |
| 参考文献 | 第90-94页 |
| 作者在学期间取得的学术成果 | 第94-95页 |
| 附录A 体系结构产品目录 | 第95-96页 |
