非交互式Petri网可覆盖性验证的高效实现 被引量：3

1

作者 丁如江 李国强 《软件学报》 EI CSCD 北大核心 2019年第7期1939-1952,共14页

近年来,基于Petri网可覆盖性的验证技术已经成功地应用于并发程序的验证与分析中。然而,由于Petri网的可覆盖性问题复杂度太高,这类技术在应用时有较大的局限性,对于输入规模较大的问题常常会出现超时的情况。而Petri网的一个子系统非... 近年来,基于Petri网可覆盖性的验证技术已经成功地应用于并发程序的验证与分析中。然而,由于Petri网的可覆盖性问题复杂度太高,这类技术在应用时有较大的局限性,对于输入规模较大的问题常常会出现超时的情况。而Petri网的一个子系统非交互式Petri网,其可覆盖性和可达性复杂性均是NP完备的,同时表达力又可以作为某类并发程序的验证模型。设计并实现了可以高效验证非交互式Petri网可覆盖性的工具CFPCV。采用基于约束的方法,从模型中提取约束,并使用Z3 SMT求解器对约束进行求解,同时,通过子网可标记方法对候选解进行验证,从而保证每组解都是正确解。通过实验分析了该工具的成功率、迭代次数以及运行效率,发现该算法不仅验证成功率高,而且性能非常优异。 展开更多

关键词 非交互式Petri网 可覆盖性 验证 模型检测 SMT求解器

下载PDF 职称材料

基于通信Petri网的异步通信程序验证模型 被引量：3

2

作者 杨启哲 李国强 《软件学报》 EI CSCD 北大核心 2017年第4期804-818,共15页

由于多栈的模型图灵等价,因此,通用的异步通信程序模型的验证问题不可判定.为此,基于Petri网,提出了一个新的模型通信——通信Petri网,对异步通信程序进行刻画.通过对输入通信进行k-型限制以及对每个栈进行基于正则语言泵引理的抽象,通... 由于多栈的模型图灵等价,因此,通用的异步通信程序模型的验证问题不可判定.为此,基于Petri网,提出了一个新的模型通信——通信Petri网,对异步通信程序进行刻画.通过对输入通信进行k-型限制以及对每个栈进行基于正则语言泵引理的抽象,通过将这样限制下的模型编码到数据Petri网,证明了限制下的新模型可覆盖性可判定. 展开更多

关键词 异步通信程序 通信Petri网 可覆盖性 程序验证 k-型

下载PDF 职称材料

良结构下推系统的可覆盖性问题的下界

3

作者 李春淼 蔡小娟 李国强 《软件学报》 EI CSCD 北大核心 2018年第10期3009-3020,共12页

良结构下推系统是下推系统和良结构迁移系统的结合,该系统允许状态和栈字符是向量的形式,因而它们是无限的.状态迁移的同时允许栈进行入栈出栈的操作.它"非常接近不可判定的边缘".利用重置0操作,提出了一种模型可覆盖性问题... 良结构下推系统是下推系统和良结构迁移系统的结合,该系统允许状态和栈字符是向量的形式,因而它们是无限的.状态迁移的同时允许栈进行入栈出栈的操作.它"非常接近不可判定的边缘".利用重置0操作,提出了一种模型可覆盖性问题复杂度下界的一般性证明方法,并且证明了状态是三维向量的子集和一般性的良结构下推系统的可覆盖性问题分别是Tower难和Hyper-Ackermann难的. 展开更多

关键词 良结构下推系统 可覆盖性 下界 重置0 Hyper-Ackermann难

下载PDF 职称材料

有限维线性空间的可覆盖性

4

作者 蒋田仔 《纺织基础科学学报》 1989年第1期18-20,共3页

关键词 有限维 线性空间 可覆盖性

下载PDF 职称材料

一般域上有限维线性空间的可覆盖性

5

作者 徐忠明 《纺织基础科学学报》 1989年第1期21-24,共4页

关键词 一般域 有限维 线性空间 可覆盖性

下载PDF 职称材料

异步多进程时间自动机的可覆盖性问题

6

作者 刘立 李国强 《软件学报》 EI CSCD 北大核心 2017年第5期1080-1090,共11页

已有的实时系统模型无法动态创建新进程.为此,基于时间自动机模型,提出了异步多进程时间自动机模型,将每个进程抽象为进程时间自动机,其部分状态能够触发新进程.考虑到队列会导致模型图灵完备,进程都被缓存在集合中,但仍可建模许多实时... 已有的实时系统模型无法动态创建新进程.为此,基于时间自动机模型,提出了异步多进程时间自动机模型,将每个进程抽象为进程时间自动机,其部分状态能够触发新进程.考虑到队列会导致模型图灵完备,进程都被缓存在集合中,但仍可建模许多实时系统.通过将其编码到可读边时间Petri网,证明了该模型的可覆盖性问题可判定. 展开更多

关键词 实时 异步多进程时间自动机 时间自动机 可读边时间Petri网 可覆盖性

下载PDF 职称材料

基于面向对象时间Petri网的智能电商物流服务系统建模 被引量：11

7

作者 朱正月 陈增强 《智能系统学报》 CSCD 北大核心 2018年第2期303-313,共11页

电商物流服务系统是一种集商流、物流、信息流和资金流于一体的大规模复杂系统,具有离散事件动态系统的一般特征。将面向对象技术与Petri网相结合,引入时间因素,应用于大规模复杂信息系统建模上,不仅能降低系统模型复杂度,还可以针对模... 电商物流服务系统是一种集商流、物流、信息流和资金流于一体的大规模复杂系统,具有离散事件动态系统的一般特征。将面向对象技术与Petri网相结合,引入时间因素,应用于大规模复杂信息系统建模上,不仅能降低系统模型复杂度,还可以针对模块性能做定量分析。在分析研究电商物流服务系统主要功能和Petri网理论的基础上,给出了一种面向对象时间Petri网(OOTPN)的形式定义,描述了电商物流服务系统的主要对象和业务流程,采用面向对象时间Petri网构建了电商物流服务系统的OOTPN模型,分析了子网的相关时间特性,利用可覆盖性树、关联矩阵对子网的可达性、有界性、守恒性等性质进行了分析,证明了模型系统的可靠性和健壮性,体现了OOTPN模型具有模块化、图形化、结构化特点和可扩展、可重用、易于维护等特性。 展开更多

关键词 面向对象 时间PETRI网 电商物流 智能服务系统 业务流程 可覆盖性树 关联矩阵 建模

下载PDF 职称材料

基于Petri网的协议分析技术及工具 被引量：4

8

作者 邓莹 古天龙 《桂林电子工业学院学报》 2002年第1期6-11,共6页

研究基于 Petri网的协议分析技术及工具并对要开发的协议分析器工具软件进行需求分析和人机交互界面设计 ,进而阐述该工具主要功能模块实现的思路和算法 ,并将其应用于对 AB通讯协议的描述和性能测试分析 。

关键词 PETRI网 协议分析器 AB通讯协议 P/T网 关联矩阵 可达树 可覆盖性树 不变量

下载PDF 职称材料

基于面向对象Petri网的设备采购管理系统建模及性能分析 被引量：4

9

作者 刘炎培 彭晓红 +1 位作者 舒远仲 陈志勇 《计算机工程与科学》 CSCD 北大核心 2010年第10期157-160,共4页

传统的设备采购系统不能随外界环境的变化而进行相应的重组。为此,本文提出了一种基于面向对象Petri网的设备采购系统的工作流模型。该模型将各个对象的内部结构进行封装,避免了相互之间的库所与变迁的定义干涉。模型具有模块化、图形... 传统的设备采购系统不能随外界环境的变化而进行相应的重组。为此,本文提出了一种基于面向对象Petri网的设备采购系统的工作流模型。该模型将各个对象的内部结构进行封装,避免了相互之间的库所与变迁的定义干涉。模型具有模块化、图形化、结构化的特性,提高了设备采购系统的可重用性和可扩展性。以审批部门的OOPN模型为例,求其关联矩阵、可覆盖性树和P不变量,并进行相关性分析,证明了构建的模型具有良好的性能并满足系统变化和重组的要求。 展开更多

关键词 面向对象 PETRI网 设备采购系统 可覆盖性树 关联矩阵

下载PDF 职称材料

Petri网的反向展开及其在程序数据竞争检测的应用 被引量：3

10

作者 郝宗寅 鲁法明 《软件学报》 EI CSCD 北大核心 2021年第6期1612-1630,共19页

展开技术借助分支进程可在一定程度上缓解Petri网性质分析中的状态爆炸问题.但展开网中仍然包含了系统的所有状态信息.某些应用问题仅需对系统特定状态的可覆盖性进行判定,以此为目标,有望缩减网系统展开的规模.为此,针对安全Petri网的... 展开技术借助分支进程可在一定程度上缓解Petri网性质分析中的状态爆炸问题.但展开网中仍然包含了系统的所有状态信息.某些应用问题仅需对系统特定状态的可覆盖性进行判定,以此为目标,有望缩减网系统展开的规模.为此,针对安全Petri网的可覆盖性判定问题提出了一种目标导向的反向展开算法,结合启发式技术缩减展开的规模,以此提高目标标识可覆盖性判定的效率.进而,将反向展开算法应用于并发程序的形式化验证,将并发程序的数据竞争检测问题转换为Petri网特定标识的可覆盖性判定问题.实验对比了正向展开与反向展开在Petri网可覆盖性判定问题上的效率,结果表明:当Petri网展开的正向分支较多时,反向展开相比正向展开具有更高的可覆盖性判定效率.最后,对影响反向展开效率的关键因素做了分析与总结. 展开更多

关键词 PETRI网 可覆盖性判定 反向展开 启发式优化 数据竞争检测

下载PDF 职称材料

基于Petri网的协同三维建模工作流模型研究 被引量：1

11

作者 魏爽 赵红领 +1 位作者 张涛 王宗敏 《计算机应用研究》 CSCD 北大核心 2009年第9期3300-3303,共4页

通过分析大规模三维场景单机建模所面临的局限性问题,对三维场景协同建模理论进行了描述。结合workflow net的定义以及建立工作流模型的方法,采用基于Petri网扩展的、用于复杂工作流模型设计的建模方法建立协同三维建模的工作流模型,并... 通过分析大规模三维场景单机建模所面临的局限性问题,对三维场景协同建模理论进行了描述。结合workflow net的定义以及建立工作流模型的方法,采用基于Petri网扩展的、用于复杂工作流模型设计的建模方法建立协同三维建模的工作流模型,并通过Petri网相关理论分析得出所建模型具有可达性、有界性、活性,并且是安全可靠的,同时对系统中必须加以解决的并发问题进行了相关的探讨。 展开更多

关键词 协同建模 PETRI网 工作流 可达性 可覆盖性树

下载PDF 职称材料

无界时延混合Petri网(UTHPN)的可覆盖性演变图及性质 被引量：1

12

作者 赵义军 王培良 《系统仿真学报》 CAS CSCD 2003年第z1期53-55,共3页

时延混合Petri网(THPN)是由David最早提出的一类混合Petri网模型,而构造时延混合Petri网的演变图是对其性质进行分析的有效方法. 赵义军等在文[1]中给出了有界时延混合Petri网的演变图构造方法及性质分析,但对无界的时延混合Petri网,其... 时延混合Petri网(THPN)是由David最早提出的一类混合Petri网模型,而构造时延混合Petri网的演变图是对其性质进行分析的有效方法. 赵义军等在文[1]中给出了有界时延混合Petri网的演变图构造方法及性质分析,但对无界的时延混合Petri网,其演变图却不能用同样的方法构造出来.在本文中,通过引入无界量符号w,给出了UTHPN的可覆盖性演变图的构造方法,并在此基础上讨论了UTHPN的有关性质. 展开更多

关键词 无界时延混合Petri网 不变行为状态 可覆盖性演变图 动态性质

下载PDF 职称材料

基于Petri网理论建立办公网收、发文管理系统协作模型

13

作者 马辉 《重庆职业技术学院学报》 2006年第4期157-160,共4页

办公信息系统是不同于一般信息系统的一类特殊的信息系统,因而办公系统的建模也有其特殊性。本文主要通过建立基于Petri网理论的办公网收、发文管理系统协作模型,分析得出所建模型具有可达性、有界性、活性,并且是安全可靠的,完全符合... 办公信息系统是不同于一般信息系统的一类特殊的信息系统,因而办公系统的建模也有其特殊性。本文主要通过建立基于Petri网理论的办公网收、发文管理系统协作模型,分析得出所建模型具有可达性、有界性、活性,并且是安全可靠的,完全符合办公信息系统需求;同时指出该模型中反映的必须在系统中加以解决的并发问题。 展开更多

关键词 PETRI网 协作模型 可覆盖性树 办公管理信息系统

下载PDF 职称材料

无穷状态系统可覆盖性分析算法

14

作者 张龙 屈婉霞 +1 位作者 郭阳 李思昆 《计算机辅助设计与图形学学报》 EI CSCD 北大核心 2018年第6期1145-1151,共7页

针对良序结构迁移系统可覆盖性分析计算成本高的问题,提出一种运用有限状态模型检验技术解决无穷状态系统可覆盖性问题的算法.首先将良序结构迁移系统划分为不同权值限定下的一系列有限状态机模型;然后采用最新的模型检验技术增量式地... 针对良序结构迁移系统可覆盖性分析计算成本高的问题,提出一种运用有限状态模型检验技术解决无穷状态系统可覆盖性问题的算法.首先将良序结构迁移系统划分为不同权值限定下的一系列有限状态机模型;然后采用最新的模型检验技术增量式地计算不同权值下模型的可达状态空间上逼近,得到可覆盖的反例路径或证明该系统不可覆盖.实验结果表明,该算法在同等计算时间限制下能够解决更多的测试样例;在1 GB内存限制下,可以解决97.2%的测试样例,超过同类算法的2倍. 展开更多

关键词 良序结构迁移系统 无穷状态系统 可覆盖性分析 PETRI网 IC3

下载PDF 职称材料