搜索结果: 1-15 共查到“计算机科学技术 模型检测”相关记录21条 . 查询时间(0.254 秒)
量子马尔可夫链安全性模型检测
量子马尔可夫链 模型检测 安全性 量子有穷自动机 广义量子loop程序
2014/1/6
本文定义了量子线性时间属性,包括量子安全性,量子不变性,讨论了它们的关系和性质.结合测量一次、测量多次的单向量子有穷自动机,构建了两类乘积量子马尔可夫链,提出了基于自动机技术的量子正则安全性检测方法.通过验证乘积量子马尔可夫链的可达终状态来判断量子正则安全性的可满足性,并给出了可满足性的概率计算公式.作为应用,分析了广义量子loop程序,将程序终止归结为验证量子正则安全性的可满足性.
基于模型检测的工作流访问控制策略验证
工作流 访问控制 策略策略验证 模型检测
2010/2/1
访问控制策略的有效性对工作流管理系统的安全稳定运行具有重要影响，针对这一问题，提出了一种基于模型检测的工作流管理系统访问控制策略验证方法。建立了工作流管理系统的访问控制策略模型与工作流执行主体任务权限状态模型，并在此基础上对访问控制策略的有效性进行验证。实验表明该算法具有有效性和合理性，为访问控制策略的验证提供了一条新的解决途径。
基于Groebner基的模型检测技术及其工具实现
符号模型检测 Groebner基 多项式环
2009/11/30
为了减少运算复杂度和运算时间，优化检测的性能，使得计算过程更加快速高效，在符号化模型检测的过程中，利用Groebner基进行多项式约化，设计出新的模型检测算法。并且基于该算法开发出新的符号模型检测工具。该工具能更快速地验证各软件及硬件系统的性质，具有较高的实用价值。
模型检测和评定在动态虚拟生物建模中的应用
虚拟生物模型 检测 差异度评定
2009/10/10
针对现在虚拟生物模型中存在真实度不够，构造的模型特征不能满足自然的生物法则等问题，根据系统模型的复杂度，模型内的各要素之间存在着很强的交互性和协作性等特点，提出了一种基于模型检测和特征差异度评定的动态虚拟生物建模方法。这种方法缩小了所构建的模型和真实生物特征之间的差距，从而提高了用户在虚拟现实系统中的沉浸感；并通过实验证实了该构造模型机制的可行性和有效性。
基于层次单元划分的软件模型检测技术研究
软件模型检测 层次单元划分 引导式搜索
2009/9/21
通过对近年来软件模型检测领域流行的几种技术进行综述，提出了一种基于层次单元划分，使用引导式搜索方式的软件模型检测方案。本方案分为预处理、单元划分、状态空间搜索三个阶段，其中使用on-the-fly技术提高了搜索性能。实验证明，该方案在解决状态爆炸问题上有较好的效果。
并行化是提高模型检测效率的重要手段。该文研究了基于标号迁移系统的C程序模型检测，提出一种软件模型检测并行化的方法。该方法利用软件模型检测工具模块化验证(MAGIC)的模块化特性对C程序进行组件分解，将各组件均衡地分发到若干计算节点，由节点调用MAGIC完成验证。由于保证节点间只有少量的通信与同步，该方法能达到较好的并行加速比，具有良好的可扩展性。实验结果显示，该方法大幅压缩了检测时间，有利于大规模...
基于符号化模型检测的对弈必胜策略验证
二值判定图 对弈 必胜策略
2009/7/17
在对弈的研究中，验证对弈双方是否存在必胜策略的问题一直没能很好地解决，因为这涉及到超大规模的状态空间搜索。而随着符号化模型检测技术的发展，大规模系统的验证成为了可能。给出了使用符号化模型检测来验证对弈必胜策略的一般方法，并给出了一个井字棋必胜策略验证的实例。
模型检测迷惑二进制恶意代码
反汇编 恶意代码 自动机
2009/7/14
对二进制恶意代码进行形式化建模，开发了一个检查迷惑恶意代码的模型检查器。生成迷惑前的二进制恶意代码的有限状态机模型，再使用模型检查器检测迷惑二进制恶意代码，如果迷惑二进制恶意代码能被有限状态机模型识别，可判定其为恶意代码。实验结果表明模型检查迷惑二进制恶意代码是一种有效的静态分析方法，可以检测出一些常用的迷惑恶意代码。
基于SPIN的IKEv2协议高效模型检测
模型检测 SPIN Promela IP隧道
2009/6/24
论文先简单介绍了互联网密钥交换协议IKEv2，然后利用著名的模型检测工具SPIN对其进行了建模和分析。在建模的过程中，作者发现现有的建模方法很难对结构复杂的协议IKEv2进行建模，而且用现有的建模方法建立的模型可读性差、自动化程度不高，验证效率也比较低，因此现有的建模方法只适用于对简单协议进行建模。针对这些不足之处，提出了一种程序可读性、自动化程度及验证效率均较好的建模方法，而且这种建模方法特别适...
概率非否认协议的模型检测分析
非否认 PRISM 有限状态机
2009/4/30
基于概率模型检测技术，建立了需要保证ε-公平性的非否认协议的概率模型，根据不同行为将主体建立有限状态机模型。使用概率模型检测器PRISM，验证了概率非否认协议的有效性、公平性和时限性。在恶意实体能力和网络环境等不同情况下，分析了破坏协议公平性的概率。
UML模型检测方法的研究
模型检测 统一建模语言 层次自动机 简单进程元语言解释器
2009/2/24
统一建模语言（UML）是设计和分析软件系统最常用的方法，如何保证UML模型满足某些特性是一个非常重要的问题，而模型检测是一种能够有效提高系统可靠性的自动化技术。研究了使用简单进程元语言解释器（SPIN）对UML模型进行检测的方法。首先对UML模型进行形式化描述，使用层次自动机来描述状态图，然后根据层次自动机的操作语义将状态图和类图的部分信息转化为SPIN的输入语言PROMELA，使用SPIN来验证...
具有过去时态算子的计算树逻辑模型检测
计算树逻辑 模型检测 二叉判定图
2009/2/23
在计算树逻辑(CTL)中引入过去时态算子，得到了表达力更强的属性规约语言CTLP，给出了CTLP 的模型检测算法及其固定点刻画。该算法的复杂性和CTL一样。固定点刻画使得CTLP的符号模型检测过程能够实现，从而有效克服了模型检测中的状态爆炸问题。
研究了利用模型检测技术对WPDL描述的工作流模型的正确性的检测方法，提出了工作流模型的正确性检测指标及其CTL*公式描述，以及博弈算法实现工作流模型的正确性检测，该方法的特点是具有较强的检测指标描述能力及高效的检测算法。
一种有效的基于LTL和Petri网的模型检测方法
模型检测 线性时序逻辑 自动机
2008/12/16
模型检测的一个主要方法是构建线性与时序逻辑（LTL）公式φ的否定形式等价的Büchi自动机Aφ和系统模型M的正交积，并检测正交积的可接受语言是否为空。通过对Generalized Büchi自动机进行化简，可以减小自动机的状态空间，从而提高模型检测的效率。根据所提出的方法设计并实现的基于LTL和Petri网进行模型检测的工具包，可以有效地对基于Petri网表示的系统模型进行模型检测。
传值进程模型检测中诊断信息的生成
2007/11/2
AbstractAutomatic
diagnostic information generation is one of the remarkable advantages of model
checking methods. It is very important to understand the reason for the failure
and fix the problem....