一种支持并行离散事件仿真建模和并行模型检验的建模语言

• 作者: 夏薇 姚益平 慕晓冬
• 来源期刊: 国防科技大学学报
• 学科: 工学
• 关键词: 并行离散事件仿真 模型检验 事件图 逻辑进程范型 DVE建模语言 模型转换
• 年，卷（期）: 2011,（6）
• 所属期刊栏目: 计算机工程·电子工程
• 页码范围: 66-71
• 分类号: TP391
• 字数: 4193字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-2486.2011.06.011

摘要

并行离散事件仿真(Parallel Discrete Event Simulation,PDES)模型的正确性和可信度对PDES应用的发展起着决定性作用.然而,现有的并行离散事件仿真开发环境都没有提供仿真模型检验功能.并行模型检验(Parallel Model Checking,PMC)方法以其完备性、高效性已经在工业界中得到了成功的应用,但是PDES和PMC是基于不同的建模语言实现的,现阶段要对PDES模型进行验证需要专门设计基于PMC建模语言的模型,不仅耗费资源、时间,而且容易出错.为了实现PDES和PMC的有机结合,提出了一种支持PDES和PMC的统一的建模语言——扩展事件图(Extended Event Graph,EEG),它对事件图在模型同步方面进行了扩展,然后通过转换机制,该建模语言使得用户只需建立一个模型,就能够既进行PDES又利用并行模型检验方法对PDES模型进行形式化验证.最后通过实验验证了基于EEG建立的模型既可以进行PDES又能够进行PMC.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	姚益平	国防科技大学计算机学院	54	382	10.0	17.0
2	夏薇	国防科技大学计算机学院	8	36	4.0	5.0
4	慕晓冬	第二炮兵工程大学计算机系	64	234	8.0	9.0