论文部分内容阅读
针对目前缺乏描述和分析C^3I系统的理论基础，提出了基于时间自动机理论的C^3I系统的数学模型．建立了C^3I系统中各个子系统的时间自动机模型，子系统之间通过通道进行通讯，通过时间自动机网把C^3I系统构建为多个并行的时间自动机的网络模型．提出基于计算树逻辑CTL的C^3I系统的实时性表达方法，详细描述使用模型检测工具Uppaal对C^3I系统建模和所建模型的实时性验证的方法．实验结果证明，基于时间自动机的C^3I系统的建模与模型检测方法是有效的，为C^3I系统行为的分析、验证提供理论基础．与经典算法相比