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

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

Modeling of a C3I system and its real time performance and verification based on timed automata network

There is no a complete way which can describe and analyze the dynamic behaviors of a C3I(command,control,communication,and intelligence) system.Hence a timed automata model of C3I systems is presented in this paper.The timed automata models for all subsystems of C3I system are developed.The subsystems communicate through passages.The timed automata network divides a C3I into several parallel timed automatas.This paper proposes a real-time expression method of C3I system based on computation tree logic(CTL),and demonstrates how to make a real-time verification on the model of C3I by use of real-time model checking tool-Uppaa1.The modeling method presented in this paper is more efficient than classical algorithms for modeling and analyzing the dynamic behavior of a C3I system.