| 引用本文: | 夏薇,姚益平,慕晓冬.一种支持并行离散事件仿真建模和并行模型检验的建模语言.[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[点击复制] |
|
| |
|
|
| 本文已被：浏览 6896次 下载 5816次 |
| 一种支持并行离散事件仿真建模和并行模型检验的建模语言 |
| 夏薇1,2, 姚益平1, 慕晓冬3 |
|
(1.国防科技大学 计算机学院，湖南 长沙 410073;2. 第二炮兵工程大学 计算机系，陕西 西安 710025;3.2.第二炮兵工程大学 计算机系，陕西 西安 710025)
|
| 摘要: |
| 并行离散事件仿真(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。 |
| 关键词: 并行离散事件仿真 模型检验 事件图 逻辑进程范型 DVE建模语言 模型转换 |
| DOI： |
| 投稿日期：2011-06-16 |
| 基金项目:国家自然科学基金资助项目(61170047,61170048)；国家教育部博士点基金资助项目(200899980004) |
|
| Modeling Language for the Integration of Parallel Discrete Event Simulation Modeling and Parallel Model Checking |
| XIA Wei1,2, YAO Yiping1, MU Xiaodong3 |
|
(1.College of Computer, National Univ. of Defense Technology, Changsha 410073, China;2.
2.Department of Computer Science, Xi’an Hi-Tech Institute, Xi’an 710025, China;3.2.Department of Computer Science, Xi’an Hi-Tech Institute, Xi’an 710025, China)
|
| 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. |
| Keywords: parallel discrete event simulation model checking event graph logical process paradigm Distributed and Parallel Verification Environment modeling language model transformation |
|
|
|
|
|
