Abstract: When planning operational plan commanders often need to consider the time constraint problem between tasks. At present time constraints analysis methods for combat mission always have such problems as less type or small suitable areas. Based on this situation the paper constructs an operational task model to define the relative and absolute time of the combat mission constraints. The formal verification method to verify the time constraint of operational task is proposed, and a combat mission model to NuSMV language transformation algorithm is designed, and based on temporal logic methods are given to describe the basic time constraints such as the absolute and relative time constraints. As an example, a landing operation task is given to verify the properties of the relative and absolute constraints, and the model is corrected based on the result.

Key words: operational task, temporal constraints, consistency verification, NuSMV

摘要： 制定作战计划时往往需要考虑作战任务的时间约束问题。目前对作战任务的时间约束分析方法都存在约束类型少、验证方法适用范围小等问题。为此提出基于业务流的作战任务时间约束建模方法，构建了作战任务流模型并用以描述作战任务的相对和绝对时间约束。提出了作战任务的时间约束形式化验证方法，设计了作战任务模型到NuSMV语言的转换算法，并基于时序逻辑给出了作战任务的基本时间约束描述方法。最后以登岛作战任务为例，验证了其相对约束和绝对约束的部分性质，并根据反馈结果对模型进行了修正。

关键词: 作战任务, 时间约束, 一致性验证, NuSMV