主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2019年第10期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
夏薇,姚益平,慕晓冬,柳林.基于事件图的离散事件仿真模型并行检验方法.软件学报,2012,23(6):1429-1443
基于事件图的离散事件仿真模型并行检验方法
Parallel Model Checking for Discrete Event Simulation Models Based on Event Graphs
投稿时间:2010-11-29  修订日期:2011-02-17
DOI:10.3724/SP.J.1001.2012.04047
中文关键词:  离散事件仿真模型验证  并行模型检验  事件图  DVE 建模语言  模型转换
英文关键词:discrete event simulation model verification  parallel model checking  event graph  DVE modeling language  model transformation
基金项目:国家自然科学基金(61170048); 国家教育部博士点基金(200899980004)
作者单位E-mail
夏薇 国防科学技术大学 计算机学院,湖南 长沙 410073
第二炮兵工程大学,陕西 西安 710025 
weiwei32329@163.com 
姚益平 国防科学技术大学 计算机学院,湖南 长沙 410073  
慕晓冬 第二炮兵工程大学,陕西 西安 710025  
柳林 海军装备研究院,北京 100161  
摘要点击次数: 2702
全文下载次数: 3536
中文摘要:
      非形式化仿真模型验证方法易受主观因素的影响且具有不完备性,而传统的形式化模型检验方法由于受到状态空间爆炸问题的影响,很难处理大规模的仿真模型.并行模型检验方法以其完备性、高效性已经在工业界中得到了成功的应用,但是由于涉及到形式化规约、逻辑学以及并行计算等多项技术,应用难度较大.针对上述问题,提出了基于事件图的离散事件仿真模型并行检验方法.该方法首先对事件图在模型同步方面进行了扩展,给出了扩展事件图的形式化定义、语法及语义;然后将扩展事件图模型转换到分布并行验证环境的DVE 模型,成功地将并行模型检验方法应用于仿真模型验证领域.该方法使得仿真人员无须学习新的形式化验证语言就能采用并行模型检验方法对仿真模型进行形式化验证,可降低模型并行验证的难度,从而有效提高模型验证的效率和完备性.实验结果表明了该方法的有效性,有利于扩展并行模型检验方法在仿真领域中的应用.
英文摘要:
      Informal verification methods for simulation models are vulnerable to subjective ingredients. The traditional model checking method has difficulty dealing with large-scale simulation models because of the state space explosion. The parallel model checking (PMC) method has been accepted and successfully implemented in industrial tools because of the completeness and high efficiency. Unfortunately, it is hard to use as it involves several difficulties, such as formal specifications, logics, and parallel computing. To solve the above problems, a parallel model checking method for simulation models based on event graphs is proposed in this paper. This method extends event graphs in synchronization and defines the syntax and semantics of the extended event graphs. It transforms the extended event graphs to distributed and parallel verification environment (DVE) model, and PMC method is successfully applied to simulation model verification filed. With this method, simulation participators can verify simulation models with PMC method without learning new formal modeling languages. The efficiency and completeness of simulation model verification are improved. The experimental results show the validity of this method, and the method can improve the application of PMC method in simulation field.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利