PN2MSVL:工作流网到MSVL的转换

• 全文链接
• 请求原文

作   者：

师亚;  段振华;  田聪; 

作者机构：

中国计算机学会(CCF);  西安电子科技大学ISN国家重点实验室;  西安电子科技大学计算理论与技术研究所; 

关键词：

工作流网;  Petri网;  验证;  转换;  仿真;  建模; 

期刊名称：

计算机学报

基金项目：

基于APTL的开放系统模型检测
基于共享变量的多核并发程序模型检测
开放软件系统的基础理论与关键技术
实时安全关键系统的建模、仿真与验证
可信网络交易软件系统试验环境与示范应用
形式化验证
基于定理证明的多核并行程序验证

i s s n：

0254-4164

年卷期：

2014 年 37 卷 12 期

页   码：

2433-2442

摘   要：

现有的工作流网到程序设计语言的转换所生成的程序不仅可读性较差而且难以进行验证.针对这一情况,该文给出了一个工作流网到建模、仿真和验证语言(MSVL)的结构化转换工具PN2MSVL.该文首先定义了注释工作流网,然后以注释工作流网为中间模型,利用一组转换规则不断地压缩注释工作流网中的正规结构,最终得到MSVL程序.PN2MSVL生成的MSVL程序不仅具备更好的可读性,而且可以利用MSVL的支持工具MSV进行建模、仿真和验证.另外,该文通过一个应用实例详细地展示了PN2MSVL的执行过程,并通过大量的实验分析了PN2MSVL的可用性.