概率计算树逻辑的限界模型检测 被引量：15

1

作者 周从华 刘志锋 王昌达 《软件学报》 EI CSCD 北大核心 2012年第7期1656-1668,共13页

为了缓解概率计算树逻辑模型检测中的状态空间爆炸问题,提出了概率计算树逻辑的限界模型检测技术.该技术首先定义概率计算树逻辑的限界语义,并证明其正确性;之后,通过实例说明在传统限界模型检测中,以路径长度作为判断检测过程终止的标... 为了缓解概率计算树逻辑模型检测中的状态空间爆炸问题,提出了概率计算树逻辑的限界模型检测技术.该技术首先定义概率计算树逻辑的限界语义,并证明其正确性;之后,通过实例说明在传统限界模型检测中,以路径长度作为判断检测过程终止的标准已经失效,基于数值计算中牛顿迭代法的终止准则,设计了新的终止判断标准;然后提出基于线性方程组求解的限界模型检测算法;最后,通过3个测试用例说明,概率计算树逻辑限界模型检测方法在反例较短的情况下能够快速完成检测过程,而且比概率计算树逻辑的无界模型检测算法所需求得的状态空间要少. 展开更多

关键词 模型检测 限界模型检测 概率计算树逻辑 马尔可夫链

在线阅读 下载PDF 职称材料

基于自动机的概率计算树逻辑验证方法

2

作者 纪明宇 王海涛 陈志远 《计算机工程》 CAS CSCD 2013年第12期285-289,共5页

根据带有随机特征的复杂信息系统性质验证的需求,针对离散概率回报模型的分层直到公式,提出一种性质验证分析方法。在综合各种离散随机逻辑的基础上,使用一种同时具有迁移回报及迁移步区间表达能力的概率计算树逻辑表示系统模型的分层... 根据带有随机特征的复杂信息系统性质验证的需求,针对离散概率回报模型的分层直到公式,提出一种性质验证分析方法。在综合各种离散随机逻辑的基础上,使用一种同时具有迁移回报及迁移步区间表达能力的概率计算树逻辑表示系统模型的分层直到路径公式性质,使用自动机技术建模路径公式,通过构造积模型完成模型与自动机的同步演化,基于积模型给出相应的状态概率满足算法。实例结果验证了该方法的可行性和有效性。 展开更多

关键词 模型检测 分层直到公式 概率计算树逻辑 马尔可夫链 自动机 积模型

在线阅读 下载PDF 职称材料

基于概率模型检测的软件缺陷定位方法 被引量：5

3

作者 任胜兵 陈军 +1 位作者 谭文钊 左兴 《计算机应用研究》 CSCD 北大核心 2021年第11期3387-3392,3397,共7页

软件缺陷的存在导致软件无法满足用户的需求,如何高效高质量地定位缺陷是消除软件缺陷的关键。基于模型的缺陷定位技术是当前的研究热点,可以用于检测软件系统故障找到软件失效的原因。现有基于模型的缺陷定位技术中,未考虑非相邻节点... 软件缺陷的存在导致软件无法满足用户的需求,如何高效高质量地定位缺陷是消除软件缺陷的关键。基于模型的缺陷定位技术是当前的研究热点,可以用于检测软件系统故障找到软件失效的原因。现有基于模型的缺陷定位技术中,未考虑非相邻节点间传递依赖和测试用例对可疑度的影响,导致缺陷定位精度和效率低。提出了基于概率模型检测的软件缺陷定位方法(probabilistic model checking method for software fault location,PMC-SFL),首先提出一种程序概率模型用于提高模型的推理能力;然后设计了基于执行路径构建程序概率模型的学习算法;最后设计了基于概率模型检测的软件缺陷定位算法,用于缺陷定位分析。通过在公共数据集Siemens上进行实验和分析,表明了PMC-SFL方法与五种现有的缺陷定位方法RankCP、BNPDG、Tarantula、SOBER和CT相比,具有更高的软件缺陷定位精度和效率。 展开更多

关键词 缺陷定位 概率模型检测 测试用例 执行轨迹 概率计算树逻辑

在线阅读 下载PDF 职称材料

动态环境下基于概率模型检测的路径规划方法 被引量：6

4

作者 夏春蕊 王瑞 +3 位作者 李晓娟 关永 张杰 魏洪兴 《计算机工程与应用》 CSCD 北大核心 2016年第12期5-11,94,共8页

提出了一种动态复杂环境下采用概率模型检测技术进行路径规划的新方法。考虑到实际应用中机器人其移动行为总是受到外界因素的影响,将机器人移动行为看作一个不确定事件,提取环境中的影响因素,构建马尔可夫决策过程模型。采用时态逻辑... 提出了一种动态复杂环境下采用概率模型检测技术进行路径规划的新方法。考虑到实际应用中机器人其移动行为总是受到外界因素的影响,将机器人移动行为看作一个不确定事件,提取环境中的影响因素,构建马尔可夫决策过程模型。采用时态逻辑语言描述机器人目标任务,表达复杂多样的需求行为。运用工具PRISM验证属性,得到满足任务需求的全局优化路径。另外,在全局路径的基础上提出了一种动态避障策略,实现避障局部规划的同时尽量保证机器人最大概率完成任务。通过理论和仿真实验结果证明该方法的正确性和有效性。 展开更多

关键词 路径规划 动态障碍物 概率模型检测 马尔可夫决策过程 概率计算树逻辑

在线阅读 下载PDF 职称材料

概率模型检测技术在机器人路径规划中的应用 被引量：2

5

作者 夏春蕊 王瑞 +1 位作者 李晓娟 关永 《计算机仿真》 CSCD 北大核心 2015年第3期364-369,共6页

在机器人路径规划的实际应用中,针对机器人移动行为可能会受到外界环境影响的难题,提出了一种采用概率模型检测技术进行路径规划的新方法。首先,分析环境中的主要影响因素,将机器人的移动行为看作一个不确定事件,构建马尔可夫决策过程(M... 在机器人路径规划的实际应用中,针对机器人移动行为可能会受到外界环境影响的难题,提出了一种采用概率模型检测技术进行路径规划的新方法。首先,分析环境中的主要影响因素,将机器人的移动行为看作一个不确定事件,构建马尔可夫决策过程(MDP)模型。然后,采用概率计算树逻辑(PCTL)公式描述模型属性,表达机器人复杂多样的目标任务。最后,运用PRISM平台对模型进行分析和验证,得到满足属性的全局优化路径和定量数据。仿真结果表明,上述方法不仅能够保障机器人在障碍物环境中无碰撞移动,而且可以避开环境相对复杂的区域,保证机器人以最大概率完成任务。对比试验证明上述方法的正确性和有效性。 展开更多

关键词 移动机器人 路径规划 概率模型检测 马尔可夫决策过程 概率计算树逻辑

在线阅读 下载PDF 职称材料

面向概率ZIA时序及度量性质的检测研究 被引量：1

6

作者 倪水妹 曹子宁 《小型微型计算机系统》 CSCD 北大核心 2015年第3期550-555,共6页

带数据约束的概率系统是指一种既带有概率约束,又带有数据变量约束的计算系统,应用非常广泛.对这类系统而言,确保其正确性和可靠性是至关重要的.目前对带数据约束的概率系统模型的规范及验证研究较少,本文提出了一种针对概率系统的带数... 带数据约束的概率系统是指一种既带有概率约束,又带有数据变量约束的计算系统,应用非常广泛.对这类系统而言,确保其正确性和可靠性是至关重要的.目前对带数据约束的概率系统模型的规范及验证研究较少,本文提出了一种针对概率系统的带数据约束的规范.对于传统的时序逻辑如计算树逻辑和概率计算树逻辑来说,尽管这些逻辑很强大,但是只能反映系统的时序性质,为了解决这些局限性,本文提出一个新的形式化语言来表达度量性质查询,同时保留表达时序性质的能力.最后,文章给出针对概率系统度量性质的检测算法并通过实例说明本文提出的方法可行有效. 展开更多

关键词 数据约束 概率系统 概率计算树逻辑 度量性质

在线阅读 下载PDF 职称材料

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

7

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

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

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

在线阅读 下载PDF 职称材料

基于马尔科夫决策过程的可适变业务流程建模及分析 被引量：3

8

作者 张红霞 邹华 +1 位作者 林荣恒 杨放春 《电子与信息学报》 EI CSCD 北大核心 2013年第7期1760-1765,共6页

研究移动网络的适变业务流程的建模和模型分析对于部署和执行Web服务应用有着重要的意义。该文通过定义业务流程的相似性及数据类型的相容性,为可适变应用提供了候选集合,使得业务流程能够根据环境的变化动态地进行适变。为了有效地对... 研究移动网络的适变业务流程的建模和模型分析对于部署和执行Web服务应用有着重要的意义。该文通过定义业务流程的相似性及数据类型的相容性,为可适变应用提供了候选集合,使得业务流程能够根据环境的变化动态地进行适变。为了有效地对适变业务流程实例进行分析,该文提出基于马尔科夫决策过程模型的适变业务流程建模方法,采用随机模型检测技术对模型的合理性进行验证和预测。针对具体实例,采用该文提出的方法对视频传输应用进行建模和分析验证,实验结果表明,该文为适变业务流程的建模和分析验证提供了一种有效的方法。 展开更多

关键词 移动网络 业务流程 马尔科夫决策过程 概率计算树逻辑 随机模型检测

在线阅读 下载PDF 职称材料

基于模型检测的系统生存性分析 被引量：2

9

作者 周清雷 张兵 席琳 《计算机工程》 CAS CSCD 2012年第17期38-41,共4页

提出一种采用模型检测进行系统生存性分析的形式化方法。给出系统所处环境及主要提供的服务,引入灾难和错误等因素,建立系统生存性模型。通过描述系统的可生存能力,确定其生存性需求并转换为相应的逻辑表示。以电话接入网络为例,利用PR... 提出一种采用模型检测进行系统生存性分析的形式化方法。给出系统所处环境及主要提供的服务,引入灾难和错误等因素,建立系统生存性模型。通过描述系统的可生存能力,确定其生存性需求并转换为相应的逻辑表示。以电话接入网络为例,利用PRISM对系统进行建模及验证,结果表明,该形式化方法可以规范并简化生存性分析过程。 展开更多

关键词 生存性分析 形式化方法 模型检测 PRISM检测工具 离散马尔科夫链 概率计算树逻辑

在线阅读 下载PDF 职称材料

模型检测在完整性形式化验证中的应用研究 被引量：1

10

作者 严亚伟 周雁舟 惠文涛 《计算机工程与应用》 CSCD 北大核心 2017年第4期59-63,134,共6页

对于信息系统而言,数据信息的安全性是十分重要的,数据的完整性是数据安全最重要的表现形式。为了确保系统中数据信息的安全性,提高系统可靠性,需要对数据的完整性进行分析和验证。针对数据完整性的定量评估问题,提出使用概率计算树逻... 对于信息系统而言,数据信息的安全性是十分重要的,数据的完整性是数据安全最重要的表现形式。为了确保系统中数据信息的安全性,提高系统可靠性,需要对数据的完整性进行分析和验证。针对数据完整性的定量评估问题,提出使用概率计算树逻辑对完整性定义进行形式化描述,并建立相应的马尔可夫决策过程定量评估模型,运用概率模型检测算法对完整性进行的评估,实现对完整性的定量验证。通过把提出的评估模型应用于交互式电子手册系统,定量计算出了该系统模型的完整性,为系统开发中的完整性需求提供支持。 展开更多

关键词 完整性 形式化 概率分析 概率计算树逻辑 模型测试

在线阅读 下载PDF 职称材料

一种嵌入式软件可靠性建模与评估方法 被引量：1

11

作者 刘维维 庄毅 李蜜 《计算机与现代化》 2017年第8期78-83,共6页

虽然AADL已经被广泛应用于嵌入式软件体系结构的建模与分析,但其作为一种半形式化建模语言,不能满足严格分析评估软件可靠性的要求。为了解决这个问题,本文首先采用离散时间马尔可夫链DTMC刻画AADL可靠性模型,主要描述系统的状态转移与... 虽然AADL已经被广泛应用于嵌入式软件体系结构的建模与分析,但其作为一种半形式化建模语言,不能满足严格分析评估软件可靠性的要求。为了解决这个问题,本文首先采用离散时间马尔可夫链DTMC刻画AADL可靠性模型,主要描述系统的状态转移与转移概率。然后基于概率计算树逻辑PCTL提出一种可靠性定量评估方法,通过计算可用度评估可靠性。最后设计可靠性评估器,并通过一个飞行管理系统的实例研究验证所提出的建模与评估方法的有效性。 展开更多

关键词 可靠性 体系结构分析与设计语言 离散时间马尔可夫链 概率计算树逻辑 模型检测

在线阅读 下载PDF 职称材料

基于随机模型检验的社交网络隐私保护研究

12

作者 刘阳 高世国 《计算机工程》 CAS CSCD 北大核心 2021年第5期144-153,共10页

针对现有社交网络所提供静态隐私策略的隐私设置不够灵活且难以定量验证问题,提出一种动态隐私保护框架,将社交网络建模为离散时间马尔科夫链模型,通过设置触发条件实现用户动态隐私规约并将其转化为概率计算树逻辑公式,同时结合随机模... 针对现有社交网络所提供静态隐私策略的隐私设置不够灵活且难以定量验证问题,提出一种动态隐私保护框架,将社交网络建模为离散时间马尔科夫链模型,通过设置触发条件实现用户动态隐私规约并将其转化为概率计算树逻辑公式,同时结合随机模型检验和运行时验证中的参数化与监控技术,保护社交网络发生随机故障情况下的用户动态隐私信息。在Diaspora开源社交网络上的实验结果表明,与静态隐私保护框架相比,动态隐私保护框架具有更高的安全性和灵活性,能较好满足用户的隐私保护需求。 展开更多

关键词 社交网络 隐私保护 运行时验证 随机模型检验 概率计算树逻辑

在线阅读 下载PDF 职称材料

智能合约函数的建模与验证研究

13

作者 叶昊榀 刘阳 《计算机仿真》 北大核心 2021年第3期201-205,共5页

针对智能合约对安全性方面的相关性质的极高要求,有必要改进已有的建模算法,提出将智能合约函数的函数体语句建模为DTMC的算法,并对生成的DTMC进行验证。通过为状态迁移添加概率,实现了对随机现象的关注。通过对调用函数的分类处理,精... 针对智能合约对安全性方面的相关性质的极高要求,有必要改进已有的建模算法,提出将智能合约函数的函数体语句建模为DTMC的算法,并对生成的DTMC进行验证。通过为状态迁移添加概率,实现了对随机现象的关注。通过对调用函数的分类处理,精细化了对函数调用函数情况的处理。通过添加标识符,实现了对智能合约所有控制语句的支持。对常被用于判定函数是否可以被触发的require语句,提供了差异化的处理方式从而改善算法的处理能力。同时对智能合约应保障的部分性质进行规约以验证模型效果。实验结果表明,建模方法可以实现对智能合约所有控制结构语句建模的支持,能够实现对合约函数的建模并完成验证。 展开更多

关键词 智能合约 形式化方法 离散时间马尔可夫链 概率计算树逻辑 随机模型检验

在线阅读 下载PDF 职称材料

基于Markov Decision Processes的可靠性定量分析实证研究

14

作者 刘跃军 苏静 《安阳师范学院学报》 2017年第5期14-18,共5页

由于设备、资源和传输等不能保证具有绝对的可靠运行性,所以理论上满足用户需求的模型在实际运行中也会出现一些偏差。为了定量地衡量这种偏差,提升用户对模型的信任程度,文章提出了利用马尔科夫决策过程Markov Decision Processes(MDP)... 由于设备、资源和传输等不能保证具有绝对的可靠运行性,所以理论上满足用户需求的模型在实际运行中也会出现一些偏差。为了定量地衡量这种偏差,提升用户对模型的信任程度,文章提出了利用马尔科夫决策过程Markov Decision Processes(MDP)和PRISM定量地研究反应式系统的可靠性以及利用预测结果为用户选择适当的服务。实验结果表明:该方法能尽早地对系统模型进行评估,能为用户进行"按需选择服务"提供帮助和决策,具有一定的实用性。 展开更多

关键词 需求分析 可靠性 马尔科夫决策过程(MDP) 概率计算树逻辑 PRISM

在线阅读 下载PDF 职称材料