基于概率模型检测的Web服务组合验证 被引量：15

1

作者 王晶 戎玫 +1 位作者 张广泉 祝义 《计算机科学》 CSCD 北大核心 2012年第1期120-123,共4页

Web服务组合验证对提高软件开发效率、实现服务增值具有重要意义。为了验证服务组合的有效性,提出了一种基于概率模型检测的Web服务组合验证方法。首先采用扩展的有限自动机模型建立Web服务组合模型,并将该模型转换为Markov模型,然后采... Web服务组合验证对提高软件开发效率、实现服务增值具有重要意义。为了验证服务组合的有效性,提出了一种基于概率模型检测的Web服务组合验证方法。首先采用扩展的有限自动机模型建立Web服务组合模型,并将该模型转换为Markov模型,然后采用概率模型检测器PRISM验证服务组合的可靠性,最后通过实例进一步说明该方法的可行性。 展开更多

关键词 WEB服务组合 有限自动机 MARKOV模型 概率模型检测

下载PDF 职称材料

基于概率模型检测的SysML活动图验证方法 被引量：2

2

作者 严亚伟 周雁舟 《计算机工程与设计》 北大核心 2016年第4期928-932,共5页

针对系统建模语言(systems modeling language,SysML)活动图模型无法进行精确的形式化分析与验证的问题,在研究现有模型检测的基础上,提出使用概率模型检测器(PRISM)对SysML活动图模型进行检测的分析验证框架,并提出一种把SysML活动图... 针对系统建模语言(systems modeling language,SysML)活动图模型无法进行精确的形式化分析与验证的问题,在研究现有模型检测的基础上,提出使用概率模型检测器(PRISM)对SysML活动图模型进行检测的分析验证框架,并提出一种把SysML活动图转化为相应的PRISM可执行模型的转化规则。利用该转化规则可以把SysML活动图模型转化为概率模型检测器支持的格式,实现对模型的精确分析和定量验证。实验结果表明,该规则能够有效对SysML活动图模型进行转化,为模型检测提供支持。 展开更多

关键词 系统建模语言 活动图 模型测试 概率模型检测 概率模型检测器

下载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 职称材料

基于概率模型检测的移动应用缺陷评估 被引量：2

4

作者 张国强 殷博 +1 位作者 朱静雯 康介恢 《计算机工程与设计》 北大核心 2019年第7期1908-1914,共7页

为研究移动应用缺陷发生概率对应用缺陷的修复选择、应用程序质量评估的影响,提出一种基于概率模型检测的移动应用程序缺陷评估研究方法。生成移动应用程序的回调序列概率模型,将该模型转换为离散时间链的Markov模型,采用概率模型检测器... 为研究移动应用缺陷发生概率对应用缺陷的修复选择、应用程序质量评估的影响,提出一种基于概率模型检测的移动应用程序缺陷评估研究方法。生成移动应用程序的回调序列概率模型,将该模型转换为离散时间链的Markov模型,采用概率模型检测器PRISM计算移动应用缺陷的发生概率,通过统计分析和对比实验分析研究方法的可行性和有效性。 展开更多

关键词 移动应用 回调序列 应用缺陷 MARKOV模型 概率模型检测

下载PDF 职称材料

基于概率模型检测和遗传算法的基因调控网络的无限范围优化控制 被引量：1

5

作者 刘爽 魏欧 郭宗豪 《计算机科学》 CSCD 北大核心 2018年第10期313-319,共7页

基因调控网络是一类基本且重要的生物网络,通过对其进行控制可以实现生物系统功能的调节。在生物系统中,通过外部的干预控制构造关于基因调控网络的控制理论成为了非常热门的研究主题。目前,作为一种重要的网络模型,带有干扰且上下文相... 基因调控网络是一类基本且重要的生物网络,通过对其进行控制可以实现生物系统功能的调节。在生物系统中,通过外部的干预控制构造关于基因调控网络的控制理论成为了非常热门的研究主题。目前,作为一种重要的网络模型,带有干扰且上下文相关的概率布尔网络已经被广泛地应用于基因调控网络优化控制问题的研究中。针对无限范围的优化控制问题,文中提出了一种基于概率模型检测和遗传算法的近似最优控制策略的计算方法。首先,该方法将无限范围控制中定义的期望总成本归约为离散时间马尔科夫链上的平稳状态回报;然后,构建包含固定控制策略的带有干扰且上下文相关的概率布尔网络模型,采用带回报属性的时序逻辑公式表示固定控制策略的成本,采用概率模型检测器PRISM进行自动计算。进一步,采用遗传算法,将固定控制策略编码为遗传算法解空间中的个体,基于其控制成本,定义个体的适应度值,将PRISM作为求解器,通过在解空间上迭代地执行遗传操作获取近似最优解。将所提方法应用于WNT5A网络中,实验结果证明了该方法的有效性。 展开更多

关键词 基因调控网络 优化控制 概率模型检测 遗传算法

下载PDF 职称材料

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

6

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

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

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

下载PDF 职称材料

非确定性环境中移动机器人实时避障的概率模型检测 被引量：5

7

作者 王铭 王瑞 +3 位作者 李晓娟 关永 张杰 魏洪兴 《小型微型计算机系统》 CSCD 北大核心 2014年第9期2104-2109,共6页

移动机器人的避障问题是机器人学的重要问题,实时避障是移动机器人安全导航的关键.针对移动机器人存在的制动机误差和传感器噪声等不确定因素,采用概率模型检测的方法对实时避障控制策略进行验证和定量分析.首先,将目标机器人的避障运... 移动机器人的避障问题是机器人学的重要问题,实时避障是移动机器人安全导航的关键.针对移动机器人存在的制动机误差和传感器噪声等不确定因素,采用概率模型检测的方法对实时避障控制策略进行验证和定量分析.首先,将目标机器人的避障运动及动态障碍物的非确定运动建模为马尔科夫决策过程,其中避障策略包括等待避障、减速避障和加速避障.然后,运用概率计算树逻辑语言描述目标机器人运动的关键属性并使用概率模型检测工具进行验证.最后,分析得到目标机器人与动态障碍物发生碰撞的最大概率值;目标机器人采取减速(加速)避障时,减速(加速)行驶的最佳时间;目标机器人的控制误差对避障运动的影响等.实验结果表明某些参数影响目标机器人的避障效果,并为参数值的选择提供参考依据. 展开更多

关键词 移动机器人 控制误差 实时避障 概率模型检测 马尔科夫决策过程

下载PDF 职称材料

基于概率模型检测的机电系统动态可靠性评价 被引量：3

8

作者 侯翌 杨培林 +2 位作者 徐凯 刘青 樊娟妮 《中国机械工程》 EI CAS CSCD 北大核心 2019年第5期549-553,共5页

为克服传统动态可靠性分析方法的不足,提出基于概率模型检测的机电系统动态可靠性评价方法。介绍了概率模型检测的概念及概率模型检测工具PRISM。用形式化建模语言描述系统单元的状态变迁过程,建立了机电系统的形式化模型。利用连续随... 为克服传统动态可靠性分析方法的不足,提出基于概率模型检测的机电系统动态可靠性评价方法。介绍了概率模型检测的概念及概率模型检测工具PRISM。用形式化建模语言描述系统单元的状态变迁过程,建立了机电系统的形式化模型。利用连续随机逻辑对机电系统可靠性评价指标进行形式化描述,建立了可靠性指标的规约表达式,借助概率模型检测工具自动解算可靠性指标,实现了基于概率模型检测的机电系统动态可靠性评价。所提方法建模过程简单,能有效提高机电系统动态可靠性分析的效率。 展开更多

关键词 动态可靠性 可靠性评价 概率模型检测 机电系统

下载PDF 职称材料

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

9

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

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

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

下载PDF 职称材料

概率模型检测在动态能耗管理中的应用 被引量：1

10

作者 杜伊 何洋 洪玫 《计算机科学》 CSCD 北大核心 2018年第1期261-266,291,共7页

如何平衡嵌入式设备的能耗和性能表现,成为了一个热门话题。动态能耗管理是一种在保证系统性能的基础上降低其能耗的有效方法,其关键点是如何生成有效的动态能耗管理策略。在概率模型检测技术的基础上,提出了一种生成和验证动态能耗管... 如何平衡嵌入式设备的能耗和性能表现,成为了一个热门话题。动态能耗管理是一种在保证系统性能的基础上降低其能耗的有效方法,其关键点是如何生成有效的动态能耗管理策略。在概率模型检测技术的基础上,提出了一种生成和验证动态能耗管理策略的方法。首先对目标系统和能耗管理目标建模,然后利用PRISM-games工具进行动态能耗管理策略的合成,同时利用模型检测工具PRISM对合成的动态能耗管理策略进行验证。实验表明,该方法具备可行性和有效性。 展开更多

关键词 动态能耗管理 概率模型检测 策略合成 策略验证

下载PDF 职称材料

概率模型检测的网络传播干预策略 被引量：1

11

作者 李宙洲 魏欧 +2 位作者 郭宗豪 余鹏 韩兰胜 《小型微型计算机系统》 CSCD 北大核心 2017年第6期1175-1180,共6页

网络普遍存在于自然界和人类社会中,计算机病毒、传染疾病、森林火灾以及社会流言等在网络中的传播给经济、社会带来巨大挑战.寻找有效的干预策略实现对网络传播的控制是一个重要的研究问题.根据传播过程的内在规律,引入了概率网络传播... 网络普遍存在于自然界和人类社会中,计算机病毒、传染疾病、森林火灾以及社会流言等在网络中的传播给经济、社会带来巨大挑战.寻找有效的干预策略实现对网络传播的控制是一个重要的研究问题.根据传播过程的内在规律,引入了概率网络传播模型,将干预目标描述为相应的概率时序逻辑属性,提出了概率情况下的网络传播干预策略问题;进一步,以离散的邮件病毒传播模型为研究对象,重点分析了安装防护,定期防护两种防护措施,给出了相应的干预策略分析问题;并且,采用概率模型检测工具PRISM,结合近似模型检测方法,进行了实验分析. 展开更多

关键词 概率模型检测 网络传播干预策略 近似模型检测方法 形式化方法

下载PDF 职称材料

基于概率模型检测器的核电厂分布式控制系统动态可靠性分析 被引量：3

12

作者 夏林路 张雪松 +2 位作者 赵鹏飞 陈浠毓 周世梁 《核科学与工程》 CAS CSCD 北大核心 2022年第2期318-328,共11页

分布式控制系统(DCS)是核电厂的神经中枢,对其进行可靠性分析,识别薄弱环节,开展有针对性的设计优化和运维改进,提高电厂安全水平。DCS部件存在备用自投、在线修复等动态行为,传统故障树不能充分描述上述动态行为。针对上述问题,采用马... 分布式控制系统(DCS)是核电厂的神经中枢,对其进行可靠性分析,识别薄弱环节,开展有针对性的设计优化和运维改进,提高电厂安全水平。DCS部件存在备用自投、在线修复等动态行为,传统故障树不能充分描述上述动态行为。针对上述问题,采用马尔科夫模型建立完整的DCS子系统可靠性模型,包括操作终端、PU处理单元、交换机,以及处理器、电源等各类模件,采用概率模型检测器PRISM对马尔科夫模型进行定量计算,得到系统的不可用率,并对系统各失效状态维修率进行了敏感性分析,结果表明,操作与监视系统(OM690)、电厂总线和采集卡失效对系统不可用率的贡献高达95%,因此,通过增加OM690系统、总线设备、采集卡的备件数量和维护人力,可有效提高上述设备的可靠性。 展开更多

关键词 DCS 马尔科夫模型 概率模型检测器 转移矩阵 动态可靠性

下载PDF 职称材料

基于概率模型检测的微电网的形式化验证 被引量：1

13

作者 孙春竹 杨晋吉 《华南师范大学学报（自然科学版）》 CAS 北大核心 2018年第2期124-128,共5页

利用概率模型检测的方法对微电网电源系统建立离散时间马尔可夫链模型,在系统后续的状态迁移中加入了故障率;类比云平台弹性计算功能,添加了另一个分布式电源,并验证其对系统进程的影响;用概率计算树逻辑对微电网电源系统进行描述,并对... 利用概率模型检测的方法对微电网电源系统建立离散时间马尔可夫链模型,在系统后续的状态迁移中加入了故障率;类比云平台弹性计算功能,添加了另一个分布式电源,并验证其对系统进程的影响;用概率计算树逻辑对微电网电源系统进行描述,并对系统的负荷成本、经济成本以及状态迁移数进行定量分析.验证结果表明:分布式电源故障率对系统的收益和消耗有不同程度的影响,加上云平台的弹性计算思想在微电网上的灵活运用,可以提高微电网的性能及生产效益,对实际生产有极大的借鉴意义. 展开更多

关键词 形式化验证 概率模型检测 分布式微电网 PRISM

下载PDF 职称材料

一种高效的动态概率广播算法及其概率模型检测分析

14

作者 文英 董荣胜 《小型微型计算机系统》 CSCD 北大核心 2008年第3期417-421,共5页

在AdHoc网络中,广播有着相当广泛的应用,其算法的效率极大地影响着网络的性能.本文基于DP算法提出了BN-DP算法,考虑了节点分布、计数器值以及收发节点间距离对广播算法的影响,赋予处于接收边缘的节点更高的转发概率.然后使用概率模型检... 在AdHoc网络中,广播有着相当广泛的应用,其算法的效率极大地影响着网络的性能.本文基于DP算法提出了BN-DP算法,考虑了节点分布、计数器值以及收发节点间距离对广播算法的影响,赋予处于接收边缘的节点更高的转发概率.然后使用概率模型检测工具PRISM,分析了计数器值和节点分布对BN-DP算法性能的影响.结果表明:在相同可达率的情况下,所提出的BN-DP算法与FP、DP算法相比,减少了转发分组的数量,提高了广播效率. 展开更多

关键词 AD HOC网络 BN—DP算法 概率模型检测 PRISM

下载PDF 职称材料

一个分布式K互斥算法的概率模型检测

15

作者 刘来 骆翔宇 《计算机应用研究》 CSCD 北大核心 2015年第4期1036-1039,共4页

传统的验证方法难以保证分布式K互斥算法的有效性和安全性。为解决这一问题,给出了进一步的研究,提出一种基于概率模型检测器PRISM的方法,对Kerry Raymond的分布式K互斥算法进行形式化建模与分析验证。通过设置算法中各个进程进入临界... 传统的验证方法难以保证分布式K互斥算法的有效性和安全性。为解决这一问题,给出了进一步的研究,提出一种基于概率模型检测器PRISM的方法,对Kerry Raymond的分布式K互斥算法进行形式化建模与分析验证。通过设置算法中各个进程进入临界区的时间而得出的结果中发现,改变临界区的数目K,对于某一进程进入临界区的平均及时时间的影响并不大。如果某一进程的执行时间比其他进程大很多,则K的增加可以提高运行效率。最后证明了这一结论。 展开更多

关键词 分布式K互斥算法 概率模型检测 PRISM 平均及时时间

下载PDF 职称材料

基于概率模型检测的Web服务组合多目标验证 被引量：4

16

作者 周女琪 周宇 《计算机科学》 CSCD 北大核心 2018年第8期288-294,共7页

Web服务组合是服务计算领域的重要研究内容。用户的非功能性需求是Web服务组合中衡量服务的标准之一,然而开放环境下用户的需求具有一定的不确定性和多目标性特点。为了解决此种不确定性,提出了一种基于概率模型检测的多目标验证方法。... Web服务组合是服务计算领域的重要研究内容。用户的非功能性需求是Web服务组合中衡量服务的标准之一,然而开放环境下用户的需求具有一定的不确定性和多目标性特点。为了解决此种不确定性,提出了一种基于概率模型检测的多目标验证方法。首先,将Web服务组合过程建立为定量多目标马尔可夫决策过程,并将该模型转换为PRISM模型。同时,将不同的用户需求建模成多目标时序逻辑公式,使用概率模型检测器PRISM对其进行验证,获得多个目标约束下关键目标的期望值,并导出相关策略。最后,通过实例来进一步说明该方法的有效性与可行性。 展开更多

关键词 WEB服务组合 概率模型检测 多目标验证 用户需求

下载PDF 职称材料

Ad Hoc网络中城市街道移动模型的概率模型检测

17

作者 文英 董荣胜 《广西科学院学报》 2006年第4期252-255,共4页

应用概率模型检测技术,在M anhattan移动模型和街道单元移动模型的基础上,提出城市街道移动模型,将其建模成离散时间马尔可夫链DTM C s,然后运用概率模型检测工具PR ISM分析节点位置及移动情况对A d Hoc网络通信的影响。

关键词 AD HOC网络 城市街道移动模型 PRISM 概率模型检测

下载PDF 职称材料

基于概率模型检测的合同签订协议分析

18

作者 陈立斌 董荣胜 《桂林电子工业学院学报》 2005年第6期31-35,共5页

概率合同签订协议的公平性具有典型的概率性质。概率模型检测是一种验证存在随机行为系 统的分析技术。基于概率模型检测技术,在原协议的基础上建立了离散马尔可夫链和有限状态机模型, 用概率模型检测工具——PRISM验证了它的公平性,发... 概率合同签订协议的公平性具有典型的概率性质。概率模型检测是一种验证存在随机行为系 统的分析技术。基于概率模型检测技术,在原协议的基础上建立了离散马尔可夫链和有限状态机模型, 用概率模型检测工具——PRISM验证了它的公平性,发现其公平性不满足时,在此基础上对原协议从 双方交换信息的策略上进行了扩充改进,使协议更为公平,满足了合同签订的基本要求。 展开更多

关键词 合同签订公平性 概率模型检测 PRISM 有限状态机

下载PDF 职称材料

船体结构检测概率模型对裂纹分布更新的影响

19

作者 李典庆 张圣坤 唐文勇 《上海交通大学学报》 EI CAS CSCD 北大核心 2004年第11期1865-1869,共5页

在对现有的检测概率模型比较的基础上,提出了一种用于更新裂纹尺寸分布的检测概率模型,并且从理论上证明了大部分现有的检测概率模型都是新检测概率模型的特例.采用最小二乘法确定了检测概率模型中参数的取值,并用算例对新检测概率模型... 在对现有的检测概率模型比较的基础上,提出了一种用于更新裂纹尺寸分布的检测概率模型,并且从理论上证明了大部分现有的检测概率模型都是新检测概率模型的特例.采用最小二乘法确定了检测概率模型中参数的取值,并用算例对新检测概率模型和现有的检测概率模型进行了比较.在此基础上,将新检测概率模型用于分析船体结构裂纹尺寸分布更新的问题,采用贝叶斯更新方法分析了检测概率模型对裂纹后验分布的影响.结果表明,新检测概率模型具有更好的拟合检测数据的能力,不同的检测概率模型对裂纹的后验分布有明显的影响. 展开更多

关键词 船体结构 检测概率模型 无损检测 贝叶斯更新

下载PDF 职称材料

雷达检测概率模型研究 被引量：4

20

作者 李秀金 王坤 +1 位作者 范江涛 于卫刚 《现代电子技术》 2013年第21期18-20,共3页

针对传统雷达检测概率计算复杂性的问题,基于雷达方程和Albersheim公式,推导了任意虚警概率下雷达检测概率与目标距离之间的关系,建立了一种易于计算的雷达检测概率模型。并根据典型雷达参数,对不同虚警概率和脉冲积累时的雷达检测概率... 针对传统雷达检测概率计算复杂性的问题,基于雷达方程和Albersheim公式,推导了任意虚警概率下雷达检测概率与目标距离之间的关系,建立了一种易于计算的雷达检测概率模型。并根据典型雷达参数,对不同虚警概率和脉冲积累时的雷达检测概率模型进行了仿真分析,仿真结果准确可信。该模型对敌我攻防作战的规划具有一定的参考价值。 展开更多

关键词 Albersheim公式 检测概率模型 虚警概率 脉冲积累 仿真分析

下载PDF 职称材料