一种支持并行离散事件仿真建模和并行模型检验的建模语言
DOI:
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:

国家自然科学基金资助项目(61170047,61170048);国家教育部博士点基金资助项目(200899980004)


Modeling Language for the Integration of Parallel Discrete Event Simulation Modeling and Parallel Model Checking
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    并行离散事件仿真(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。

    Abstract:

    The correctness and reliability of parallel discrete event simulation models play an important role in the development of PDES. Most of the existing PDES developing environments do not support model verification at present. The completeness and high effectiveness of parallel model checking helps it successful in making its way into industrial tools. While PDES and PMC are implemented in different modeling languages, in the current practice, to check whether or not a PDES model contains any errors, a prototype that is solely written for model checking purposes has to be built. This process is an onerous, time-consuming and error-prone task. The current research presented a modeling language, namely Extended Event Graph (EEG) to combine PDES and PMC, and it extended the classical event graph in aspect of synchronization. This modeling language makes it possible for users to achieve PDES and PMC with only one model via transformation mechanisms, thus saving both the time and effort of developers. The experimental results confirm the validity of this language and it can support both PDES and PMC.

    参考文献
    相似文献
    引证文献
引用本文

夏薇,姚益平,慕晓冬.一种支持并行离散事件仿真建模和并行模型检验的建模语言[J].国防科技大学学报,2011,33(6):66-71.
XIA Wei, YAO Yiping, MU Xiaodong. Modeling Language for the Integration of Parallel Discrete Event Simulation Modeling and Parallel Model Checking[J]. Journal of National University of Defense Technology,2011,33(6):66-71.

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2011-06-16
  • 最后修改日期:
  • 录用日期:
  • 在线发布日期: 2012-09-12
  • 出版日期:
文章二维码