论文部分内容阅读
并行离散事件仿真（Parallel Discrete Event Simulation，PDES）模型的正确性和可信度对PDES应用的发展起着决定性作用。然而，现有的并行离散事件仿真开发环境都没有提供仿真模型检验功能。并行模型检验（ParallelModelChecking，PMC）方法以其完备性、高效性已经在工业界中得到了成功的应用，但是PDES和PMC是基于不同的建模语言实现的，现阶段要对PDES模型进行验证需要专门设计基于PMC建模语言的模型，不仅耗费资源、时间，而且容易出错。为了实现PDES和PM