检索结果-南通市图书馆

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

在线全文

学校读者我要写书评

暂无评论

软件学报 2012年第11期23卷 2835-2861页

作者：周从华叶萌王昌达刘志锋江苏大学计算机科学与通信工程学院江苏镇江212013

为了形式化描述多智体系统中与概率、实时、知识相关的性质,提出了一种概率实时认知逻辑PTCTLK.模型检测是验证多智体系统是否满足PTCTLK公式的主要技术,状态空间爆炸是该技术实用化的主要瓶颈,为此提出一种PTCTLK的限界模型检测算法.... 详细信息

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

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

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

在线全文

学校读者我要写书评

暂无评论

计算机科学 2006年第6期33卷 1-6,100页

作者：陈铭松赵建华李宣东郑国梁南京大学计算机软件新技术国家重点实验室南京大学计算机科学与技术系南京210093

时间自动机是检验实时系统建模的有效工具,其可达性分析可以检验系统是否可能达到某些特定的状态,其算法通常采用对符号状态的枚举来遍历其状态空间。因为引入了时钟变量,时间自动机的可达性分析算法会产生大量的中间状态,需要巨大的存... 详细信息

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

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

在线全文

学校读者我要写书评

暂无评论

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

中国电子科学研究院学报 2023年第2期18卷 166-175,188页

作者：李东方刘诗宇王纪王志昊闫皓中国航天科工集团第二研究院706所北京100854

在实际工业验证场景中,形式化验证的局限性主要体现在因为状态空间爆炸导致验证结果不明确。断言编码方式始终是直接影响到形式化验证结果的主要因素,而目前已有的断言优化方法并未以断言与状态空间大小的关系分析为基础。文中针对影响... 详细信息

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

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

在线全文

学校读者我要写书评

暂无评论

面向工业互联网的攻击图生成及分析方法研究

面向工业互联网的攻击图生成及分析方法研究

作者：沈霄梦南京林业大学

学位级别：硕士

随着“工业4.0”时代的到来,工业互联网与人工智能、数字孪生等先进信息技术相结合,在能源、交通、工业制造等关键领域发挥了重要作用。与此同时,原本大规模孤立的工业设备接入工业互联网,带来了严重的安全问题。如何在防御资源受限的... 详细信息

随着“工业4.0”时代的到来,工业互联网与人工智能、数字孪生等先进信息技术相结合,在能源、交通、工业制造等关键领域发挥了重要作用。与此同时,原本大规模孤立的工业设备接入工业互联网,带来了严重的安全问题。如何在防御资源受限的情形下对工业互联网中的大量漏洞进行安全防护已成为亟待解决的重要问题。针对该问题,现有研究主要采用基于全局攻击图的漏洞评估方法,借助通用漏洞评分系统进行漏洞的量化指标分析。然而,该类方法难以避免状态空间爆炸问题,并且缺乏对于漏洞所处工业互联网环境的评估,严重局限已有方法的应用。为此,本文面向工业互联网研究基于局部攻击图的最小关键漏洞集分析方法以及基于概率攻击图的漏洞修复策略分析方法。主要研究内容如下:(1)基于局部攻击图的最小关键漏洞集分析方法研究为了集中优势资源防御系统中的关键漏洞,提出了一种基于局部攻击图的最小关键漏洞集分析方法。以系统当中的重要资产节点为目标,裁剪目标不可达的攻击路径,生成由可入节点到目标节点的局部攻击图,并根据生成过程中得到的路径漏洞集进行最小关键漏洞集的分析。实验结果表明,基于局部攻击图的最小关键漏洞集分析方法能够有效缓解状态空间爆炸,节省攻击图二次遍历的时空开销,在网络规模较大时能显著提高关键漏洞的分析效率。(2)基于概率攻击图的漏洞修复策略分析方法研究为了进一步确定关键漏洞修复的优先级顺序,提出了一种基于概率攻击图的漏洞修复策略分析方法。针对工业互联网中的漏洞修复优先级进行评估,在量化过程中引入可见性、可控性度量和环境因子,根据防御效益对漏洞修复的优先级进行排序,并对系统漏洞的防御策略进行概率模型检测。相关工作对比结果表明,相较于传统的漏洞评估方法,所提方法在工业互联网领域更具适用性,能够有效选取具有最优防御效益的漏洞进行修复。(3)工具实现与实例分析研究基于本文所提出的理论,开发了一款面向工业互联网的攻击图生成与分析工具。该工具集成了攻击图构建、攻击图可视化生成、定性与定量分析漏洞的功能。为了验证该工具的可用性,选取火力发电厂的辅助车间集中控制系统作为实例应用。分析结果表明,本文方法合理可行,能够在防御资源受限的条件下,为选取关键漏洞进行防御提供有效依据。

关键词：工业互联网局部攻击图最小关键漏洞集状态空间爆炸概率攻击图

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

面向随机模型检验的模型抽象技术

软件学报 2015年第8期26卷 1853-1870页

作者：刘阳李宣东马艳计算机软件新技术国家重点实验室(南京大学) 江苏南京210093 Department of computer Science School of ComputingNational University of Singapore 南京航空航天大学计算机科学与技术学院江苏南京210016

随机模型检验是经典模型检验理论的延伸和推广,由于其结合了经典模型检验算法和线性方程组求解或线性规划算法等,并且运算处理的是关于状态的概率向量而非经典模型检验中的位向量,所以状态爆炸问题在随机模型检验中更为严重.抽象作为缓... 详细信息

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

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

在线全文

学校读者我要写书评

暂无评论

马尔可夫决策过程的限界模型检测

计算机学报 2013年第12期36卷 2587-2600页

作者：周从华邢支虎刘志锋王昌达江苏大学计算机科学与通信工程学院江苏镇江212013

限界模型检测避免了符号模型检测反应式系统中构建二叉图时出现的空间快速增长,已经被证明是缓解状态空间爆炸问题的有力技术.文中遵循限界模型检测的思想,对马尔可夫决策过程提出一种限界模型检测技术,从而避免构建多端二叉图时空间的... 详细信息

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

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

在线全文

学校读者我要写书评

暂无评论

采用CPAChecker的动态程序验证

西安电子科技大学学报 2019年第1期46卷 33-38页

作者：段钊刘锟龙西安电子科技大学计算机学院陕西西安710071 合肥工业大学电气与自动化工程学院安徽合肥230009

针对模型检测中状态空间爆炸问题,在CPAChecker的抽象谓词检测方法的基础上,提出了一种基于动态执行的检测方法.首先,根据程序的控制流程图,对程序进行静态检测。在静态检测的过程中,根据分支语句的确定性,利用动态执行的方法来加快检... 详细信息

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

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

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

在线全文

学校读者我要写书评

暂无评论

电子学报 2013年第7期41卷 1343-1351页

作者：刘志锋孙博周从华江苏大学计算机科学与通信工程学院江苏镇江212013

概率实时时态认知逻辑PTACTLK模型检测面临着与传统模型检测同样的挑战,即状态空间爆炸问题.抽象是缓解状态空间爆炸问题的最为有效的方法之一.为了缓解概率实时时态认知逻辑模型检测中的状态空间爆炸问题,我们给出了一种抽象技术:对于P... 详细信息

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

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

在线全文

学校读者我要写书评

暂无评论

协议分布式测试系统的性能模型

高技术通讯 2003年第8期13卷 1-7页

作者：刘鸿吴建平清华大学计算机科学与技术系北京100084

协议测试领域专家们已经达成共识 :新一代的协议测试系统应该是分布式架构的。本文用广义随机Petri网 (GSPN )对目前提出的几种协议分布式测试框架构造了性能模型 ,进行了性能比较和分析。为了解决状态空间爆炸的问题 ,提出了一种同步... 详细信息

协议测试领域专家们已经达成共识 :新一代的协议测试系统应该是分布式架构的。本文用广义随机Petri网 (GSPN )对目前提出的几种协议分布式测试框架构造了性能模型 ,进行了性能比较和分析。为了解决状态空间爆炸的问题 ,提出了一种同步变迁实施速率等价法 (STER) ,这种方法能够对具有同步变迁的随机Petri网模型分解求解。

关键词：协议测试分布式系统 Petri网性能模型状态空间爆炸同步变迁实施速率等价法