共查询到17条相似文献,搜索用时 78 毫秒
1.
2.
基于时序逻辑模型检测的入侵检测技术降低了误用检测的漏报率,然而却几乎不能描述并发攻击和分段攻击,因而对这些复杂的攻击模式漏报率仍很高。本文针对该问题,提出了一种基于投影时序逻辑模型检测的入侵检测方法。对若干复杂攻击实例的检测表明,新方法可有效降低对并发攻击和分段攻击的漏报率。 相似文献
3.
李均涛 《数字社区&智能家居》2013,(26):5820-5821,5832
运用假设行为时序逻辑理论体系对磁盘的文件系统进行描述,建立入侵系统模型,使用模型检测工具予以取证。该方法的目标是在反侦察攻击环境下,即在证据缺失的情况下,也能顺利地进行取证调查。 相似文献
4.
基于攻击树的网络攻击建模方法 总被引:6,自引:3,他引:6
攻击树(AttackTree)是一种具有树表示结构的网络攻击建模工具。它具有结构化、可重用的优点。已有一些工作在它的基础上展开。但总的来说,现有的研究都着重于针对具体的攻击事件进行建模,在利用攻击树进行分析时缺乏系统性和整体性,难以对攻击树进行有效的利用。该文利用攻击树从系统的角度来对攻击进行建模,并尝试利用建模后得到的攻击树对系统整体的安全性进行分析与评估;此外,通过对攻击过程进行阶段划分,大大降低了构造出的攻击树的复杂度,使得攻击树更易于使用、分析和维护。实例分析表明,该方法能很好地刻画网络攻击的特征,可以为系统的安全分析和评估提供比较令人满意的指导,具有较好的实用性。 相似文献
5.
6.
模型检测技术在实时系统验证中被广泛使用。离散时间区间时序逻辑满足性是可判定的,因而也是可模型检测的。连续时间域时间区间时序逻辑是否可模型检测,则并不清楚。约束时间域到非负实数,证明了其可满足性是不可判定的,但存在该逻辑的可判定子集,并发现了这样的子集。由于模型检测问题可归约为时序逻辑满足性判定问题,因此结果表明,时间区间时序逻辑不可模型检测,但其可判定子集可模型检测。 相似文献
7.
王勤思 《计算机工程与设计》2011,32(2):568-571,575
在实时系统的形式验证中,为了直接验证带有明显时间约束的性质,选用了一种被广泛接受的(线性时间)实时时序逻辑——度量区时序逻辑来描述待验证的性质;提出了基于迁移的扩展时间B chi自动机;构建了度量区时序逻辑的基于迁移的扩展时间B chi自动机。这样扩展了已有实时系统模型检测工具的性质规范语言的表达能力,使其能直接处理和验证带有明显时间约束的性质。实现的工具表明,该算法有效且可行,并且显著地减少了结果自动机节点和迁移的数量,从而降低了结果自动机的大小,有利于进一步的模型检测过程。 相似文献
8.
工作流系统中的活动是与时间有着紧密联系的,如何保证恰当的活动在恰当时间被执行是工作流系统中的关键问题。探讨了如何利用时序逻辑来解决上述问题,提出了工作流系统中有效性的概念,给出了基于时序逻辑的有效性约束模型,并利用模型检测技术提供了验证有效性约束的方法,最后给出一个实例说明该方法的正确性。 相似文献
9.
为了能够将哲学逻辑中的公理系统运用到行为时序逻辑的研究中。对行为时序逻辑公式的语义进行形式化定义.从语义和语法两方面研究行为时序逻辑公理系统和具有自反性质的线性时序逻辑公理系统之间的联系.提出并证明行为时序逻辑公式转换为自反线性时序逻辑公式的定理。按照集合论和模型论的思想,定义行为时序逻辑中项和行为时序逻辑原子公式的概念。定义Lesilie Lamport所提出的行为时序逻辑公式的语义。证明自反线性时序逻辑公理系统适用于行为时序逻辑公理系统.以此为基础证明行为时序逻辑的简单规则、基本规则和附加规则。 相似文献
10.
基于时序Petri网的联锁逻辑形式建模与验证 总被引:1,自引:0,他引:1
时序Petri网结合Petri和时序逻辑的优点,清晰简洁地描述并发系统事件间的时序和因果关系,包括系统的最终性和公平性。文章给出安全苛求系统——车站信号联锁逻辑系统的时序Petri网描述,并使用时序逻辑描述系统状态的时序和因果关系,最后通过分析和验证模型的性质得出系统是正确的。 相似文献
11.
该文详细介绍了统一建模语言和模型检测技术,在此基础上,该文研究了基于交互自动机和时态逻辑的UML交互模型性质检测方法,提出了模型检测所需的Marking算法。该算法通过对交互自动机全部状态的遍历,检测各状态的时态逻辑公式(CTL公式)的真值,以判断用户设计的UML交互模型是否符合计算机软件系统应满足的性质及规范。 相似文献
12.
13.
14.
SPIN模型检测器主要用来检测线性时序逻辑描述的规范,而多智体系统的规范采用时序认知逻辑描述比较方便。本文着重讨论了如何利用SPIN模型检测线性时序认知逻辑的方法,根据局部命题的理论,将模型检测知识算子和公共算子表述的规范规约为模型检测线性时序逻辑的问题,从而使SPIN的检测功能由线性时序逻辑扩充到线性时序认知逻辑。本文通过一个RPC协议分析实例来说明模型检测线性时序认知逻辑的方法。 相似文献
15.
基于自动机理论的模型检测技术在形式化验证领域处于核心地位, 然而传统自动机在时态算子上不具备可组合性, 导致各种时态逻辑的模型检测算法不能有机整合.本文为了实现集成限界时态算子的实时分支时态逻辑RTCTL*的高效模型检测, 提出一种RTCTL*正时态测试器构造方法, 以及相关符号化模型检测算法.证明了所提出的RTCTL*正时态测试器构造方法是完备的.也证明了该算法时间复杂度与被验证系统呈线性关系, 与公式长度呈指数关系.我们基于JavaBDD软件包成功开发了该算法的模型检测工具MCTK 2.0.0.我们完成了MCTK与著名的符号化模型检测工具nuXmv之间的实验对比分析工作, 结果表明MCTK虽然在内存消耗上要多于nuXmv, 但是MCTK的时间复杂度双指数级小于nuXmv, 使得利用MCTK验证大规模系统的实时时态性质成为可能. 相似文献
16.
Classical logic cannot be used to effectively reason about concurrent systems with inconsistencies (inconsistencies often occur, especially in the early stage of the development, when large and complex concurrent systems are developed). In this paper, we propose the use of a paraconsistent temporal logic (QCTL) for supporting the verification of temporal properties of such systems even where the consistent model is not available. We introduce a novel notion of paraKripke models, which grasps the paraconsistent character of the entailment relation of QCTL. Furthermore, we explore the methodology of model checking over QCTL, and describe the detailed algorithm of implementing QCTL model checker. In the sequel, a simple example is presented, showing how to exploit the proposed model checking technique to verify the temporal properties of inconsistent concurrent systems. 相似文献