基于时间自动机网的C3I系统建模和实时性验证

• 作者: 刘群 梁冰
• 来源期刊: 哈尔滨工程大学学报
• 学科: 工学
• 关键词: C3I系统 时间自动机网 模型检测 实时性验证
• 年，卷（期）: 2008,（3）
• 页码范围: 272-277
• 页数: 6页
• 分类号: TP3
• 字数: 5073字
• 语种: 中文
• DOI: 10.3969/j.issn.1006-7043.2008.03.014

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	刘群	哈尔滨工程大学计算机科学与技术学院	40	188	8.0	11.0
2	梁冰	哈尔滨工程大学计算机科学与技术学院	21	173	8.0	12.0