随机时间Petri网综述 被引量：5

1

作者 卢光松 葛运建 《计算机科学》 CSCD 北大核心 2005年第3期26-30,共5页

随机时间Petri网作为一种灵活有力的建模机制,被广泛应用于计算机和通信系统的性能与可靠性评价。综述了随机时间Petri网各主要子类的发展历程与研究现状。首先介绍了随机时间Petri网的一些基本概念,然后回顾了广义随机Petri网,简要总... 随机时间Petri网作为一种灵活有力的建模机制,被广泛应用于计算机和通信系统的性能与可靠性评价。综述了随机时间Petri网各主要子类的发展历程与研究现状。首先介绍了随机时间Petri网的一些基本概念,然后回顾了广义随机Petri网,简要总结了处理状态空间爆炸问题的主要途径,讨论了非马尔科夫随机Petri网及其分析技术,最后详细分析了流体随机Petyi网。 展开更多

关键词 随机时间Petri网 建模机制 非马尔科夫随机Petri网 分析技术 流体随机PETRI网

下载PDF 职称材料

基于同构节点的动态故障树分析方法 被引量：7

2

作者 张红林 付剑 +1 位作者 张春元 王英鸿 《计算机工程与设计》 CSCD 北大核心 2011年第1期1-4,共4页

为了解决动态故障树研究领域的马尔可夫链状态空间爆炸问题,给出了一个基于同构节点的动态故障树分析方法。为每个节点建立一个对象,识别同构节点,求解时对于同构节点仅计算一次,从而减少状态空间中的状态数目、缩短计算时间。运用该方... 为了解决动态故障树研究领域的马尔可夫链状态空间爆炸问题,给出了一个基于同构节点的动态故障树分析方法。为每个节点建立一个对象,识别同构节点,求解时对于同构节点仅计算一次,从而减少状态空间中的状态数目、缩短计算时间。运用该方法对空间信息处理平台进行可靠性分析,并与其他方法进行对比,结果表明,如果系统结构具有较强的冗余特征,该方法在求解效率上具有比较明显的优势。 展开更多

关键词 动态故障树 同构节点 空间信息处理平台 故障树分析 可靠性分析 状态空间爆炸

下载PDF 职称材料

马尔可夫决策过程的限界模型检测 被引量：7

3

作者 周从华 邢支虎 +1 位作者 刘志锋 王昌达 《计算机学报》 EI CSCD 北大核心 2013年第12期2587-2600,共14页

限界模型检测避免了符号模型检测反应式系统中构建二叉图时出现的空间快速增长,已经被证明是缓解状态空间爆炸问题的有力技术.文中遵循限界模型检测的思想,对马尔可夫决策过程提出一种限界模型检测技术,从而避免构建多端二叉图时空间的... 限界模型检测避免了符号模型检测反应式系统中构建二叉图时出现的空间快速增长,已经被证明是缓解状态空间爆炸问题的有力技术.文中遵循限界模型检测的思想,对马尔可夫决策过程提出一种限界模型检测技术,从而避免构建多端二叉图时空间的快速增长.具有非确定选择刻画能力是马尔可夫决策过程最大的特性,针对该特性首先定义概率计算树逻辑的限界语义,并证明其正确性;然后基于不同界下所计算概率度量序列的演化趋势,设计了限界检测过程终止的判断准则;最后将限界模型检测过程转换为线性方程组的求解问题.实验结果说明限界模型检测技术在证据较短的情况下,所需内存空间少于无界模型检测算法. 展开更多

关键词 模型检测 限界模型检测 概率计算树逻辑 马尔可夫决策过程 状态空间爆炸

下载PDF 职称材料

基于局部攻击图的最小关键漏洞集分析方法

4

作者 沈霄梦 徐丙凤 何高峰 《计算机工程与设计》 北大核心 2024年第6期1607-1614,共8页

为缓解攻击图应用在工业互联网安全防护中的状态空间爆炸问题,提出一种基于局部攻击图的最小关键漏洞集分析方法。提出一种以重要资产节点为目标的局部攻击图生成算法,通过裁剪不可达目标节点的攻击路径缓解状态空间爆炸问题;基于局部... 为缓解攻击图应用在工业互联网安全防护中的状态空间爆炸问题,提出一种基于局部攻击图的最小关键漏洞集分析方法。提出一种以重要资产节点为目标的局部攻击图生成算法,通过裁剪不可达目标节点的攻击路径缓解状态空间爆炸问题;基于局部攻击图生成过程中得到的攻击路径漏洞集直接进行最小关键漏洞集分析,节省传统分析方法在搜索关键漏洞过程中对攻击图进行二次遍历的时空开销。在此基础上,通过工业网络实例进行分析并开展相关工作比较,实验结果表明,所提方法合理可行,可高效分析网络系统中的最小关键漏洞集。 展开更多

关键词 工业互联网 攻击图 关键漏洞集 状态空间爆炸 网络安全 局部攻击图生成 安全防御

下载PDF 职称材料

适用于形式化验证的断言优化方法

5

作者 李东方 刘诗宇 +2 位作者 王纪 王志昊 闫皓 《中国电子科学研究院学报》 北大核心 2023年第2期166-175,188,共11页

在实际工业验证场景中,形式化验证的局限性主要体现在因为状态空间爆炸导致验证结果不明确。断言编码方式始终是直接影响到形式化验证结果的主要因素,而目前已有的断言优化方法并未以断言与状态空间大小的关系分析为基础。文中针对影响... 在实际工业验证场景中,形式化验证的局限性主要体现在因为状态空间爆炸导致验证结果不明确。断言编码方式始终是直接影响到形式化验证结果的主要因素,而目前已有的断言优化方法并未以断言与状态空间大小的关系分析为基础。文中针对影响锥模型不能分析断言中时序关系对状态空间的影响的问题,提出长序列模型,分析形式化验证中断言与状态空间大小的定性关系。在此基础上,提出适用于形式化验证的断言优化方法,方法包含断言逻辑化简、辅助验证逻辑、参考模型和断言禁用条件,并以某商用HDLC IP核为例,对比优化前后的验证结果,证明优化的有效性。 展开更多

关键词 断言优化 形式化验证 状态空间爆炸 影响锥模型 长序列模型

下载PDF 职称材料

采用CPAChecker的动态程序验证 被引量：3

6

作者 段钊 刘锟龙 《西安电子科技大学学报》 EI CAS CSCD 北大核心 2019年第1期33-38,共6页

针对模型检测中状态空间爆炸问题,在CPAChecker的抽象谓词检测方法的基础上,提出了一种基于动态执行的检测方法.首先,根据程序的控制流程图,对程序进行静态检测。在静态检测的过程中,根据分支语句的确定性,利用动态执行的方法来加快检... 针对模型检测中状态空间爆炸问题,在CPAChecker的抽象谓词检测方法的基础上,提出了一种基于动态执行的检测方法.首先,根据程序的控制流程图,对程序进行静态检测。在静态检测的过程中,根据分支语句的确定性,利用动态执行的方法来加快检测的过程。其中,抽象检测可以有效地限制系统模型的规模,动态执行不仅可以有效地减少静态检测导致的误判,而且有助于引导构建精确的系统模型,降低虚假反例的数量和不必要的反例分析和精化。实验数据显示,这种算法明显提高了传统的反例引导谓词抽象精化算法的检测效率和准确率。 展开更多

关键词 模型检测 抽象精化 动态执行 程序验证 状态空间爆炸

下载PDF 职称材料

时间自动机可达性分析中的状态空间约减技术综述 被引量：3

7

作者 陈铭松 赵建华 +1 位作者 李宣东 郑国梁 《计算机科学》 CSCD 北大核心 2006年第6期1-6,100,共7页

时间自动机是检验实时系统建模的有效工具,其可达性分析可以检验系统是否可能达到某些特定的状态,其算法通常采用对符号状态的枚举来遍历其状态空间。因为引入了时钟变量,时间自动机的可达性分析算法会产生大量的中间状态,需要巨大的存... 时间自动机是检验实时系统建模的有效工具,其可达性分析可以检验系统是否可能达到某些特定的状态,其算法通常采用对符号状态的枚举来遍历其状态空间。因为引入了时钟变量,时间自动机的可达性分析算法会产生大量的中间状态,需要巨大的存储空间,往往超出了计算机能力的极限,导致分析和检验不能完成。这就是所谓的“状态空间爆炸”。研究人员设计了很多种优化技术来约减可达性分析所需的存储空间,以解决或者缓解这个问题。本文首先介绍了时间自动机及其可达性分析的基本概念,然后分类讨论了现有的空间约减优化技术并对此做出总结,最后提出了一些未来的研究方向。 展开更多

关键词 实时系统 时间自动机 状态空间爆炸 可达性分析

下载PDF 职称材料

面向随机模型检验的模型抽象技术 被引量：2

8

作者 刘阳 李宣东 马艳 《软件学报》 EI CSCD 北大核心 2015年第8期1853-1870,共18页

随机模型检验是经典模型检验理论的延伸和推广,由于其结合了经典模型检验算法和线性方程组求解或线性规划算法等,并且运算处理的是关于状态的概率向量而非经典模型检验中的位向量,所以状态爆炸问题在随机模型检验中更为严重.抽象作为缓... 随机模型检验是经典模型检验理论的延伸和推广,由于其结合了经典模型检验算法和线性方程组求解或线性规划算法等,并且运算处理的是关于状态的概率向量而非经典模型检验中的位向量,所以状态爆炸问题在随机模型检验中更为严重.抽象作为缓解状态空间爆炸问题的重要技术之一,已经开始被应用到随机模型检验领域并取得了一定的进展.以面向随机模型检验的模型抽象技术为研究对象,首先给出了模型抽象技术的问题描述,然后按抽象模型构造技术分类归纳了其研究方向及目前的研究进展,最后对比了目前的模型抽象技术及其关系,总结出其还未能给出模型抽象问题的满意答案,并指出了有效解决模型抽象问题未来的研究方向. 展开更多

关键词 随机模型检验 状态空间爆炸 模型抽象 定量抽象精化

下载PDF 职称材料

概率实时时态认知逻辑模型检测中抽象技术的研究 被引量：2

9

作者 刘志锋 孙博 周从华 《电子学报》 EI CAS CSCD 北大核心 2013年第7期1343-1351,共9页

概率实时时态认知逻辑PTACTLK模型检测面临着与传统模型检测同样的挑战,即状态空间爆炸问题.抽象是缓解状态空间爆炸问题的最为有效的方法之一.为了缓解概率实时时态认知逻辑模型检测中的状态空间爆炸问题,我们给出了一种抽象技术:对于P... 概率实时时态认知逻辑PTACTLK模型检测面临着与传统模型检测同样的挑战,即状态空间爆炸问题.抽象是缓解状态空间爆炸问题的最为有效的方法之一.为了缓解概率实时时态认知逻辑模型检测中的状态空间爆炸问题,我们给出了一种抽象技术:对于PTACTLK中的实时部分PTACTL,采用抽象离散时钟赋值,把概率实时解释系统的无限状态空间转化成有限形式;对于PTACTLK中的认知算子K,给出了抽象状态关于智体认知等价的定义.定义了概率实时解释系统的抽象模型,给出了抽象模型上概率实时时态认知逻辑的语义,并证明了由抽象技术演绎得到的抽象模型是原始模型的上近似.最后通过一个通信协议来说明抽象技术的有效性. 展开更多

关键词 模型检测 概率实时时态认知逻辑 PTACTLK 状态空间爆炸 抽象

下载PDF 职称材料

多智体系统中约简状态空间的限界模型检测算法 被引量：2

10

作者 周从华 叶萌 +1 位作者 王昌达 刘志锋 《软件学报》 EI CSCD 北大核心 2012年第11期2835-2861,共27页

为了形式化描述多智体系统中与概率、实时、知识相关的性质,提出了一种概率实时认知逻辑PTCTLK.模型检测是验证多智体系统是否满足PTCTLK公式的主要技术,状态空间爆炸是该技术实用化的主要瓶颈,为此提出一种PTCTLK的限界模型检测算法.... 为了形式化描述多智体系统中与概率、实时、知识相关的性质,提出了一种概率实时认知逻辑PTCTLK.模型检测是验证多智体系统是否满足PTCTLK公式的主要技术,状态空间爆炸是该技术实用化的主要瓶颈,为此提出一种PTCTLK的限界模型检测算法.其基本思想是,在有限的局部可达空间中逐步搜索属性成立的证据,从而达到约简状态空间的目的.首先,将PTCTLK的模型检测问题转换为无实时算子的PBTLK的模型检测问题;其次,定义PBTLK的限界语义,并证明其正确性;然后,设计基于线性方程组求解的限界模型检测算法;最后,依据概率度量的演化规律,探索检测过程终止的判别准则.实例研究结果表明,与无界模型检测相比,在属性为真的证据较短的情况下,限界模型检测完成验证所需空间更小. 展开更多

关键词 多智体系统 模型检测 限界模型检测 状态空间爆炸

下载PDF 职称材料

测试目的引导的模型检测方法与技术研究 被引量：1

11

作者 赵会群 殷朝冉 《计算机应用研究》 CSCD 北大核心 2015年第8期2387-2390,2394,共5页

为了实现对伪代码的模型检测并且能够缓解模型检测中的状态空间爆炸问题,提出了测试目的引导的模型检测方法。该方法的基本思想是首先对伪代码进行模块划分并对每个模块进行建模,获取基本路径的集合并以流图的方式进行存储;然后利用自... 为了实现对伪代码的模型检测并且能够缓解模型检测中的状态空间爆炸问题,提出了测试目的引导的模型检测方法。该方法的基本思想是首先对伪代码进行模块划分并对每个模块进行建模,获取基本路径的集合并以流图的方式进行存储;然后利用自主开发的转换工具实现流图到国际标准语言LOTOS的转换,再利用自主开发的辅助工具μ-演算编辑器对测试目的进行描述;最后使用模型检测工具验证被测程序是否满足测试目的。实验结果表明,测试目的引导的模型检测方法能够实现对伪代码的模型检测,并且可以缓解状态空间爆炸问题。 展开更多

关键词 模型检测 状态空间爆炸 软件测试 LOTOS μ-演算

下载PDF 职称材料

软件模型检测中状态爆炸问题的解决方法 被引量：1

12

作者 屈媛媛 杜伊 《现代计算机（中旬刊）》 2017年第1期35-38,共4页

在软件模型检测中,系统所对应的状态数会随着系统大小成指数级增长,即状态空间爆炸问题。为了研究近年来该问题的解决方法,按照系统综述的方法,归类整理近年来对近年来解决状态空间爆炸的方法,并对每类方法的应用、限制以及该领域的未... 在软件模型检测中,系统所对应的状态数会随着系统大小成指数级增长,即状态空间爆炸问题。为了研究近年来该问题的解决方法,按照系统综述的方法,归类整理近年来对近年来解决状态空间爆炸的方法,并对每类方法的应用、限制以及该领域的未来发展方向进行分析和总结。 展开更多

关键词 状态空间爆炸 模型检测 文献综述

下载PDF 职称材料

基于决策图的复杂系统模型对称约减方法 被引量：1

13

作者 纪明宇 王海涛 +1 位作者 陈志远 李艳梅 《计算机工程与设计》 CSCD 北大核心 2013年第10期3685-3689,共5页

针对复杂随机系统模型检测过程中的状态空间爆炸问题,提出一种用于支持迁移回报特征描述的概率模型对称约减方法。通过引入状态集等价关系唯一表示函数,约减了原模型中的状态集尺寸;通过加入回报特征描述,改进了传统的多终端二元决策图... 针对复杂随机系统模型检测过程中的状态空间爆炸问题,提出一种用于支持迁移回报特征描述的概率模型对称约减方法。通过引入状态集等价关系唯一表示函数,约减了原模型中的状态集尺寸;通过加入回报特征描述,改进了传统的多终端二元决策图,用于表示概率回报模型中的迁移关系;基于迁移矩阵,提出了一种高效的对称约减算法,完成了迁移关系的约简。实验结果表明了该方法的可行性与有效性。 展开更多

关键词 形式化验证 模型检测 状态空间爆炸 决策图 对称约减 商模型

下载PDF 职称材料

面向测试生成的ASM模型约简研究 被引量：1

14

作者 杨羊 何柳柳 +1 位作者 尚颖 李征 《计算机工程与科学》 CSCD 北大核心 2018年第6期1084-1092,共9页

基于模型的Web应用程序测试是软件测试的一个重要方法。ASM模型从源码解析的角度,基于Web应用程序表示层建立模型,描述了Web应用程序的交互性、动态性和低耦合性。基于ASM模型的测试用例生成,考虑用户的非预期行为,在主要路径的基础上,... 基于模型的Web应用程序测试是软件测试的一个重要方法。ASM模型从源码解析的角度,基于Web应用程序表示层建立模型,描述了Web应用程序的交互性、动态性和低耦合性。基于ASM模型的测试用例生成,考虑用户的非预期行为,在主要路径的基础上,通过添加无效访问状态和无效迁移路径,扩充测试用例。然而,随着Web应用程序规模的扩大,无效访问状态和无效迁移路径的增加导致测试用例空间爆炸。在研究ASM模型的基础上,通过定义基于ASM模型测试生成的等价迁移和等价状态,合并迁移和状态,从而有效地对ASM模型进行约简,减少了无效访问状态和无效迁移路径的数量,实现测试用例空间约减。对一个实际Web应用程序系统的评估结果表明,基于模型约简的测试用例优化,有效约减了74.38%的测试用例空间,并且对原子段的覆盖率和错误检测数目没有产生影响。 展开更多

关键词 ASM模型 状态空间爆炸 模型约简 测试用例空间约减

下载PDF 职称材料

基于分解法建模的泵送系统可靠性和可用性评估 被引量：1

15

作者 李俊 王贤琳 《工程设计学报》 CSCD 北大核心 2015年第1期18-25,共8页

为解决马尔科夫模型的状态空间爆炸问题,在状态空间分解法的基础上,建立单个部件(层次3)的SPN模型,然后根据子系统的组成结构建立单个子系统(层次2)的SPN模型.将子系统SPN模型集成为系统模型(层次1),得到系统模型的可达图及缩小的等效... 为解决马尔科夫模型的状态空间爆炸问题,在状态空间分解法的基础上,建立单个部件(层次3)的SPN模型,然后根据子系统的组成结构建立单个子系统(层次2)的SPN模型.将子系统SPN模型集成为系统模型(层次1),得到系统模型的可达图及缩小的等效半马尔科夫图,按图建立系统模型的状态方程并求解,然后对系统进行可靠性和可用性评估.以泵送系统为例,验证分解法有助于解决状态空间爆炸问题,并使建模的难度和计算量减小,更易于操作. 展开更多

关键词 分解法 泵送系统 随机PETRI网 半马尔科夫模型 状态空间爆炸

下载PDF 职称材料

基于CPN的程序测试用例生成方法的研究

16

作者 郑文艳 《计算机工程与应用》 CSCD 2014年第11期39-45,共7页

采用成熟的建模仿真工具CPN tools不仅仅对程序设计语言的三种基本结构进行了建模,而且对并行程序中的并行结构也进行了建模和仿真。在不针对某些具体语言比如C语言的情况下,提出了生成测试用例的新方法,该方法对具备三种基本结构特性... 采用成熟的建模仿真工具CPN tools不仅仅对程序设计语言的三种基本结构进行了建模,而且对并行程序中的并行结构也进行了建模和仿真。在不针对某些具体语言比如C语言的情况下,提出了生成测试用例的新方法,该方法对具备三种基本结构特性的所有程序都具有普遍适用性。对具有并行结构的程序通过化简寻找测试路径。最后在生成测试用例之后,又利用CPN tools对所获得的测试用例进行选择和评价,最终确定合适的测试用例,不仅能够保证获取的测试路径是完整的而且是最优的。 展开更多

关键词 程序测试 颜色PETRI网 强连通图 测试路径 并行结构 状态空间 状态空间爆炸

下载PDF 职称材料

基于时序关系的系统失效可达图生成方法

17

作者 范亚琼 陈海燕 《计算机科学》 CSCD 北大核心 2017年第12期169-174,共6页

针对状态事件故障树生成系统可达图过程中存在的状态空间爆炸问题,提出了一种基于时序关系的系统失效可达图生成方法。通过分析触发和被触发类型事件的时序关系,对存在时序关系的事件进行排序,根据时序关系获得系统构件间的所有不可同... 针对状态事件故障树生成系统可达图过程中存在的状态空间爆炸问题,提出了一种基于时序关系的系统失效可达图生成方法。通过分析触发和被触发类型事件的时序关系,对存在时序关系的事件进行排序,根据时序关系获得系统构件间的所有不可同时到达状态对,对构件间的可同时到达状态建立笛卡尔积,获得系统的所有可同时到达状态对,根据连接表和最小割集获得系统失效的状态可达图,从而有效解决系统失效可达图生成过程中存在的状态空间爆炸问题。应用基于时序关系的系统失效可达图方法生成鱼攻系统失效可达图,实验结果验证了该方法的可行性与稳定性;同时也为表明其能有效地缓解状态空间爆炸问题,为状态事件故障树生成系统可达图提供了一种新的方法。 展开更多

关键词 状态事件故障树 时序关系 系统失效可达图 状态空间爆炸

下载PDF 职称材料

基于符号EVBDD的安全多方计算

18

作者 徐周波 俞强生 +1 位作者 古天龙 宁黎华 《计算机科学》 CSCD 北大核心 2016年第4期127-133,共7页

决策函数的有效表示是安全多方计算研究中的热点问题。符号描述技术是表示决策函数的一种新方法。针对基于代数决策图(ADD)的决策函数表示中出现的叶子节点规模膨胀以及导致协议面临的状态空间爆炸问题,引入边值二叉决策图(EVBDD)技术,... 决策函数的有效表示是安全多方计算研究中的热点问题。符号描述技术是表示决策函数的一种新方法。针对基于代数决策图(ADD)的决策函数表示中出现的叶子节点规模膨胀以及导致协议面临的状态空间爆炸问题,引入边值二叉决策图(EVBDD)技术,给出了一种基于EVBDD的决策函数表示方法。该方法首先利用EVBDD结构,将决策函数描述为EVBDD的符号化形式,避免了传统ADD表示中出现的叶子节点规模膨胀现象。然后通过添加虚节点,解决了计算路径上出现的隐私泄露问题。在此基础上,提出了EVBDD的加解密算法,并设计了一种新的基于EVBDD的安全两方计算协议。最后,对协议的正确性、安全性和效率进行了分析。结果表明,与基于代数决策图的解决方案相比,新协议在效率上有明显的提高。 展开更多

关键词 安全多方计算 决策函数 边值二叉决策图 状态空间爆炸

下载PDF 职称材料

形式概念分析在Web应用测试用例选取中的应用

19

作者 檀革苗 袁捷 +1 位作者 缪怀扣 王明辉 《计算机工程与设计》 CSCD 北大核心 2009年第17期3983-3985,4056,共4页

为了避免基于模型的Web应用测试中存在的状态组合爆炸问题,分析了经典的每个一次和基本选择的状态组合爆炸避免方法,指出了这两种方法的不足,提出了应用形式概念分析,根据给定的测试覆盖准则,精简测试用例集,避免状态组合爆炸的方法,并... 为了避免基于模型的Web应用测试中存在的状态组合爆炸问题,分析了经典的每个一次和基本选择的状态组合爆炸避免方法,指出了这两种方法的不足,提出了应用形式概念分析,根据给定的测试覆盖准则,精简测试用例集,避免状态组合爆炸的方法,并改进了Sampath的测试用例选取规则。最后根据形式概念分析的原理,开发了测试用例集精简工具,提高了测试过程的自动化程度,用实例说明了方法的有效性。 展开更多

关键词 形式概念分析 FSM模型 WEB应用测试 测试覆盖准则 状态组合爆炸

下载PDF 职称材料

随机进程代数新技术综述(英文)

20

作者 戴慧 丁杰 《软件》 2011年第8期50-60,共11页

本文以PEPA语言为例,对近年来发展起来的随机进程代数的缓解状态空间爆炸问题的新技术做一个综述.

关键词 综述 随机进程代数 PEPA 状态空间爆炸

下载PDF 职称材料