检索结果-南通市图书馆

在线全文

学校读者我要写书评

暂无评论

面向投影时序逻辑的Web服务模型检测

西安交通大学学报 2009年第4期43卷 39-43,124页

作者：王小兵段振华西安电子科技大学计算理论与技术研究所

为了满足Web服务的可靠性,利用投影时序逻辑的模型检测方法来验证Web服务.利用投影时序逻辑的一个可执行子集对OWL-S进行建模,用命题投影时序逻辑来描述期望的性质.模型M和性质P统一以投影时序逻辑来表示,通过判定M蕴含P的有效性,即判定... 详细信息

为了满足Web服务的可靠性,利用投影时序逻辑的模型检测方法来验证Web服务.利用投影时序逻辑的一个可执行子集对OWL-S进行建模,用命题投影时序逻辑来描述期望的性质.模型M和性质P统一以投影时序逻辑来表示,通过判定M蕴含P的有效性,即判定M和非P的合取的不可满足性,亦利用M和非P的正则形可构造合取式的正则图,判定合取的不可满足性,从而达到模型检测的目的.通过运行实例表明,所提模型检测器可验证Web服务系统性质,保证Web服务的可靠性.

关键词：形式逻辑投影时序逻辑 Web服务模型检测

在线全文

学校读者我要写书评

暂无评论

面向命题投影时序逻辑的安全协议模型检测

西安交通大学学报 2010年第8期44卷 30-35页

作者：杨琛段振华王小兵西安电子科技大学计算理论与技术研究所西安710071 武汉大学软件工程国家重点实验室武汉430072

针对无条件安全通信协议,特别是Russian Cards协议的安全性验证问题,提出基于命题投影时序逻辑(PPTL)的模型检测方法.根据协议构造规则建立了Russian Cards协议的ProMeLa模型;利用chop算子将多个交互事件进行顺序复合,以表达协议所期望... 详细信息

针对无条件安全通信协议,特别是Russian Cards协议的安全性验证问题,提出基于命题投影时序逻辑(PPTL)的模型检测方法.根据协议构造规则建立了Russian Cards协议的ProMeLa模型;利用chop算子将多个交互事件进行顺序复合,以表达协议所期望的通信序列;由projection算子定义了协议在该序列上的安全性质,再将该性质转为Never Claim语法结构并连同协议模型作为模型检测器SPIN的输入,以完成验证工作.验证结果表明,由协议规则构造的Russian Cards通信协议是安全可靠的,该方法也适用于一般的无条件安全通信协议的验证.

关键词：模型检测协议验证时序逻辑安全协议

在线全文

学校读者我要写书评

暂无评论

基于模型检测的半量子密码协议的安全性分析

电子科技大学学报 2017年第5期46卷 716-721页

作者：杨帆杨国武郝玉洁电子科技大学大数据研究中心成都611731 电子科技大学计算机科学与工程学院成都611731

对于密码协议而言,安全性是其最核心的关键问题,对于量子密码协议来说也一样。研究人员可以通过各种手段证明这些协议是安全的,但存在极大的困难,因为这对数学功底有着很高的要求。该文利用全自动化的技术——模型检测,采用了形式化验... 详细信息

对于密码协议而言,安全性是其最核心的关键问题,对于量子密码协议来说也一样。研究人员可以通过各种手段证明这些协议是安全的,但存在极大的困难,因为这对数学功底有着很高的要求。该文利用全自动化的技术——模型检测,采用了形式化验证方法,即基于概率的模型检测工具PRISM,来对半量子密码协议进行建模并验证其安全性。该方法避免了传统基于数学方法验证的繁杂,提高了验证的速度和效率。验证的结果也表明,当传输足够多的光子时,检测出窃听的概率无限趋近于1,和全量子密码协议一样,半量子密码协议也是安全的。

关键词：窃听模型检测 PRISM 半量子密码

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

在线全文

学校读者我要写书评

暂无评论

电子学报 2012年第10期40卷 2052-2061页

作者：周从华孙博刘志锋葛云江苏大学计算机科学与通信工程学院镇江212013 南京大学电子科学与工程学院南京210093

为缓解概率时态认知逻辑模型检测中的状态空间爆炸问题,提出了概率时态认知逻辑的三值抽象技术.具体研究内容包括:定义抽象模型及模型上概率时态认知逻辑的三值语义,依据状态空间等价划分建立初始抽象模型,并证明抽象技术对概率时态认... 详细信息

为缓解概率时态认知逻辑模型检测中的状态空间爆炸问题,提出了概率时态认知逻辑的三值抽象技术.具体研究内容包括:定义抽象模型及模型上概率时态认知逻辑的三值语义,依据状态空间等价划分建立初始抽象模型,并证明抽象技术对概率时态认知逻辑的满足性保持关系;提出概率时态认知逻辑模型检测算法;依据初始模型检测的结果,给出利用最小证据和最小反例引导的抽象系统的求精过程.最后通过Dining Cryptographer协议说明了抽象技术的应用,及其在约简系统状态空间方面的效果.

关键词：三值抽象模型检测概率时态认知逻辑反例

在线全文

学校读者我要写书评

暂无评论

软件模型检测中的抽象模型研究综述

计算机研究与发展 2015年第7期52卷 1580-1603页

作者：魏欧石玉峰徐丙凤黄志球陈哲南京航空航天大学计算机科学与技术学院南京210016 南京林业大学信息科学技术学院南京210037

抽象是解决模型检测中状态爆炸问题的一个基本方法.对近年来软件模型检测研究中所提出的一系列抽象模型进行综述.首先以抽象解释为理论框架阐述了抽象软件模型检测的各组成部分.然后根据模型的结构和功能特征,将抽象模型分为3类:1)传统... 详细信息

抽象是解决模型检测中状态爆炸问题的一个基本方法.对近年来软件模型检测研究中所提出的一系列抽象模型进行综述.首先以抽象解释为理论框架阐述了抽象软件模型检测的各组成部分.然后根据模型的结构和功能特征,将抽象模型分为3类:1)传统的用于支持自上逼近或者自下逼近的布尔Kripke结构;2)分别对应于3值和4值Kripke结构的Kripke模态迁移系统(Kripke modal transition systems,KMTS)和混合迁移系统(mixed transition system,MixTS),可同时支持自上逼近和自下逼近的抽象;3)具有超迁移关系的广义Kripke模态迁移系统(generalized Kripke modal transition system,GKMTS)和超迁移系统(hyper transition system,HTS),可提供更精确的抽象模型检测;重点分析这些模型的提出原因、相应的逼近关系、最优模型及其局限性以及抽象模型完备性的研究结果.最后,分析了目前关于抽象模型的理论和应用研究中存在的问题,给出进一步研究的方向.

关键词：抽象模型自上逼近自下逼近模型检测多值模型

在线全文

学校读者我要写书评

暂无评论

基于程序局部性引导的有界模型检测优化方法

通信学报 2018年第3期39卷 181-190页

作者：王舜杜晔韩臻刘吉强北京交通大学智能交通数据安全与隐私保护技术北京市重点实验室北京100044

基于多种模型检测方法组合的复合检测方式是当前软件模型检测领域开展研究的热点之一。在当前的研究中,提高检测的规模和检测的对象复杂程度的关键在于如何有效处理抽象的扩张和收缩。证明通过对程序模式或验证信息的利用可以加快状态... 详细信息

基于多种模型检测方法组合的复合检测方式是当前软件模型检测领域开展研究的热点之一。在当前的研究中,提高检测的规模和检测的对象复杂程度的关键在于如何有效处理抽象的扩张和收缩。证明通过对程序模式或验证信息的利用可以加快状态空间的探索速度。面向有界模型检测(BMC)加速方法展开研究,使用程序中额外的信息和知识对其处理以协助检测器删除冗余和无效的状态。在对程序局部性进行定义的基础上,对其加速性进行讨论,提出一种加速有界检测的方法和一种改进策略,对算法进行了详细描述,并通过实验验证了方法在检测效率和性能上的优越性。

关键词：模型检测 BMC 软件检测局部性优化

不确定型模糊Kripke结构的计算树逻辑模型检测

在线全文

学校读者我要写书评

暂无评论

电子学报 2018年第1期46卷 152-159页

作者：范艳焕李永明潘海玉陕西师范大学计算机科学学院陕西西安710062 青海师范大学民师院数学系青海西宁810008 泰州学院计算机科学与技术学院江苏泰州225300

本文研究了不确定型模糊Kripke结构的计算树逻辑的模型检测问题,并说明了该问题可以在对数多形式时间内解决.首先给出了不确定型模糊Kripke结构的定义,引入了模糊计算树逻辑的语法和语义.为了刻画存在量词?和任意量词在不确定型模糊Kr... 详细信息

本文研究了不确定型模糊Kripke结构的计算树逻辑的模型检测问题,并说明了该问题可以在对数多形式时间内解决.首先给出了不确定型模糊Kripke结构的定义,引入了模糊计算树逻辑的语法和语义.为了刻画存在量词?和任意量词在不确定型模糊Kripke结构中的两种语义解释,在模糊计算树逻辑语法中引入了路径量词?_(sup),?_(inf)和_(sup),_(inf),分别用于替换存在量词?和任意量词.其次讨论了基于不确定型模糊Kripke结构的计算树逻辑模型检测算法,特别地对于模糊计算树逻辑公式?_(sup)pUq,_(sup)pUq,?_(inf)pUq和_(inf)pUq分别给出时间复杂度为对数多项式时间的改进算法.

关键词：模型检测计算树逻辑模糊逻辑 Kripke结构时态逻辑

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

在线全文

学校读者我要写书评

暂无评论

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

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

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

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

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

在线全文

学校读者我要写书评

暂无评论

基于模型检测的机电系统FMEA研究

机械工程学报 2016年第16期52卷 162-168页

作者：杨培林徐凯薛冲冲贾焕如西安交通大学机械工程学院西安710049

失效模式与影响分析(Failure modes and effects analysis,FMEA)是一种重要的设计评审和可靠性评估手段,但传统FMEA是非形式化的,分析烦琐且容易出错。将形式化技术引入机电系统FMEA,提出基于模型检测的机电系统FMEA方法。基于机电系统... 详细信息

失效模式与影响分析(Failure modes and effects analysis,FMEA)是一种重要的设计评审和可靠性评估手段,但传统FMEA是非形式化的,分析烦琐且容易出错。将形式化技术引入机电系统FMEA,提出基于模型检测的机电系统FMEA方法。基于机电系统中的状态和事件,研究机电系统行为过程的形式化建模,针对单元失效建立面向FMEA的系统形式化模型;基于计算树逻辑(Computation tree logic,CTL)对机电系统的潜在故障进行形式化规约,并以潜在故障的否定命题构建待验证的系统行为属性;借助于模型检测工具遍历系统状态空间来检验系统是否满足行为属性,从而辨识系统单元失效与系统潜在故障之间的关系,实现基于模型检测的机电系统FMEA;将上述方法应用到数控机床进给系统,通过模型检测成功辨识出限位开关失效所导致的系统故障,验证了该方法的可行性。

关键词： FMEA 模型检测可靠性评价机电系统