基于高级Petri网的仿真剧情正规校核方法

Formal Verification Method of Simulation Scenario Based on High-level Petri Nets

针对仿真剧情主观校核不理想这一问题,提出了基于高级Petri网的仿真剧情正规校核方法.首先给出仿真剧情的形式化定义,并分析仿真剧情可能存在的错误类型;其次给出仿真剧情到高级Petri网的映射途径,并给出基于高级Petri网的仿真剧情校核准则和算法,此外,还给出实现仿真剧情动态校核的推理规则和机制;最后给出了一个正规校核工具框架.实际应用已经证明了该方法的有效性.

To solve the problem of unsatisfactory subjective verification for simulation scenario, a formal verification method of simulation scenario based on high-level Petri nets is presented. A formal definition of simulation scenario is given, and possible errors in simulation scenario are analyzed. Approaches to mapping simulation scenario into high-level Petri nets are proposed. Criteria and algorithms to verify simulation scenario based on high-level Petri nets are presented. Inference rules and mechanisms for dynamic verification of simulation scenario are also given. A formal verification tool framework of simulation scenario is constructed. Practical applications show that the formal verification method is effective.