检索结果-内蒙古大学图书馆

作者：张衍志吉林大学

学位级别：硕士

模型检测是一种自动化的形式化验证技术,在这种验证技术中包括模型化系统的Kripke结构,描述规范的命题时态逻辑和确定系统是否满足规范的模型检测算法三个要素。本文主要针对符号化模型检测算法进行研究,首先介绍了模型检测的特点、过... 详细信息

模型检测是一种自动化的形式化验证技术,在这种验证技术中包括模型化系统的Kripke结构,描述规范的命题时态逻辑和确定系统是否满足规范的模型检测算法三个要素。本文主要针对符号化模型检测算法进行研究,首先介绍了模型检测的特点、过程、三个要素和CTL与LTL的显式模型检测算法,最后提出了一个关于命题时态逻辑CTL*的符号化模型检测算法的框架,该框架包括用有序二元决策图符号化表示系统模型过程,用不动点理论描述时态算子过程和CTL*的符号化模型检测算法三个部分。在检测算法部分本文提出一种分解的方法将带有公平性约束的CTL*符号化模型检测问题转化为LTL或CTL的符号化模型检测问题,并通过在LTL和CTL的符号化模型检测算法中处理公平性约束,实现了对带有公平性约束的CTL*公式的符号化模型检测。最后本文基于开源的符号化模型检测工具NuSMV的源码实现了该算法框架。

关键词：时态逻辑有序二元决策图不动点符号化模型检测

来源：评论

学校读者我要写书评

暂无评论

基于符号化模型检测的对弈必胜策略验证

引用

计算机工程与应用 2008年第17期44卷 58-60页

作者：何青骆翔宇苏开乐湖南文理学院计算机科学与技术系湖南常德415000 桂林电子科技大学计算机与控制学院计算机系广西桂林541004 中山大学信息科学与技术学院计算机科学系广州510275

在对弈的研究中,验证对弈双方是否存在必胜策略的问题一直没能很好地解决,因为这涉及到超大规模的状态空间搜索。而随着符号化模型检测技术的发展,大规模系统的验证成为了可能。给出了使用符号化模型检测来验证对弈必胜策略的一般方法,... 详细信息

在对弈的研究中,验证对弈双方是否存在必胜策略的问题一直没能很好地解决,因为这涉及到超大规模的状态空间搜索。而随着符号化模型检测技术的发展,大规模系统的验证成为了可能。给出了使用符号化模型检测来验证对弈必胜策略的一般方法,并给出了一个井字棋必胜策略验证的实例。

关键词：符号化模型检测二值判定图对弈必胜策略

来源：评论

学校读者我要写书评

暂无评论

和与积数迷的符号化模型检测

引用

计算机科学 2008年第5期35卷 184-186页

作者：骆翔宇古天龙董荣胜桂林电子科技大学计算机与控制学院桂林541004

和与积是一个著名的数迷问题。采用公告逻辑对该问题进行建模,将其Kripke模型符号化表示为多智能体有限状态程序,并在其上采用一种基于局部命题解释系统语义的知识逻辑符号化模型检测算法计算该问题的所有解。在时态逻辑模型检测器NuSM... 详细信息

和与积是一个著名的数迷问题。采用公告逻辑对该问题进行建模,将其Kripke模型符号化表示为多智能体有限状态程序,并在其上采用一种基于局部命题解释系统语义的知识逻辑符号化模型检测算法计算该问题的所有解。在时态逻辑模型检测器NuSMV基础上扩展实现了本文算法,然后在相同实验平台上用动态认知建模工具DEMO对该问题进行求解。实验表明,我们的算法不仅结果正确,而且在运行效率上与DEMO相比占有绝对优势。

关键词：符号化模型检测多智能体系统时态逻辑公告逻辑

来源：评论

学校读者我要写书评

暂无评论

离散实时线性动态逻辑的符号化模型检测

引用

计算机科学 2020年第9期47卷 204-212页

作者：骆翔宇许杭娜曾昊晟陈祖希杨帆华侨大学计算机科学与技术学院福建厦门361021 华侨大学机电及自动化学院福建厦门361021

实时系统的错误往往十分危险甚至是致命的,使用模型检测来保证复杂实时系统的正确性是十分有效的。针对模型检测中传统时态逻辑无法表达实时性质和所有正则属性的问题,文中首先提出一种具有表达离散实时性质、所有正则属性能力的离散实... 详细信息

实时系统的错误往往十分危险甚至是致命的,使用模型检测来保证复杂实时系统的正确性是十分有效的。针对模型检测中传统时态逻辑无法表达实时性质和所有正则属性的问题,文中首先提出一种具有表达离散实时性质、所有正则属性能力的离散实时线性动态逻辑(Real-Time Linear Dynamic Logic,RTLDL);然后使用类似程序控制流标记的方法为RTLDL公式定义起止标记,根据起止标记关系构造时态测试器,提出基于时态测试器的RTLDL符号化模型检测算法;最后基于翻译的方法在模型检测器NuXmv上实现了所提算法,并针对护栏控制系统案例与线性动态逻辑(Linear Dynamic Logic,LDL)模型检测器MCMAS-LDLK进行实验比较。实验结果表明,无论对于LDL还是RTLDL公式的检测,提出的算法的效率均显著优于MCMAS-LDLK。

关键词：符号化模型检测时态测试器实时线性动态逻辑离散实时系统

来源：评论

学校读者我要写书评

暂无评论

实时分支时态逻辑RTCTL*符号化模型检测与树状反例生成

实时分支时态逻辑RTCTL*符号化模型检测与树状反例生成

引用

作者：黄欣玥华侨大学

学位级别：硕士

随着计算机与软件系统越来越广泛地应用于安全关键领域,为了避免潜在的严重后果,软件安全问题愈发受到重视。模型检测技术是一种有效的形式化验证方法,能够验证系统的正确性,并给出能够指示错误的信息。经典的基于自动机的模型检测中,... 详细信息

随着计算机与软件系统越来越广泛地应用于安全关键领域,为了避免潜在的严重后果,软件安全问题愈发受到重视。模型检测技术是一种有效的形式化验证方法,能够验证系统的正确性,并给出能够指示错误的信息。经典的基于自动机的模型检测中,自动机组合的困难限制了对于规约的高效构造。时态测试器是一种特殊的非确定性自动机,通过增加布尔输出变量,能够从自底向上地构造时态逻辑对应的时态测试器,运用时态测试器可以实现高效的模型检测。反例是模型检测的重要特性,但目前对于反例的研究并不足够,大部分模型检测工具生成的反例较为简单,对于带有分支的时态逻辑并不完备,且不能够方便用户理解。本文的主要工作如下: (1)提出一种RTCTL*正时态测试器的构造方法,及其对应的符号化模型检测算法,显著地提升了RTCTL*模型检测的性能。本文证明了提出的RTCTL*正时态测试器构造的完备性,并证明了模型检测算法时间复杂度与所验证模型大小线性相关,与待验证规约长度指数相关。 (2)拓展了CTL*的树状反例结构并提出了对应的反例图。本文拓展了树状反例的结构,通过为反例的节点与边附上必要的注释信息,使反例对于用户更加易于理解。 (3)提出一种基于测试器的模型检测算法为ACTL*生成完备且信息丰富的树状反例的方法。此外,反例图中的所有分支都是具有最短前缀的拉索路径。本文还采取了一些优化策略用以减少注释的数量,并尽量避免构建套索路径。 (4)开发了一个基于有序二元决策图(OBDD)的模型检测工具MCTK2,在其中实现了以上的模型检测与反例图生成算法,并与模型检测工具nu Xmv和MCMAS分别在验证性能与反例阐释效果上进行了实验比较,证明了MCTK2的优越性。

关键词：符号化模型检测时态测试器 RTCTL* 树状反例 MCTK2

来源：评论

学校读者我要写书评

暂无评论

基于符号化模型检测的安全协议验证

基于符号化模型检测的安全协议验证

引用

作者：温家栋中山大学

学位级别：硕士

目前，安全协议的验证工作主要采用各种形式化方法，如逻辑证明和模型检测。基于逻辑证明的安全协议分析在发现协议是不安全的之后不能给出现实的攻击路径，且协议的理想化过程及主观性假设往往会影响分析的结果。基于模型检测的安全协... 详细信息

目前，安全协议的验证工作主要采用各种形式化方法，如逻辑证明和模型检测。基于逻辑证明的安全协议分析在发现协议是不安全的之后不能给出现实的攻击路径，且协议的理想化过程及主观性假设往往会影响分析的结果。基于模型检测的安全协议分析虽然在近些年才开始受到人们的关注，但是其发展非常迅猛。特别是有序二叉决策树(OBDD)等符号化技术的引入有效地解决了模型检测面临的状态爆炸问题，产生了符号化模型检测技术。现在，符号化模型检测技术已经开始广泛地应用的安全协议的验证工作中，各种符号化模型检测工具，如SMV等应运而生。\n IBS (Internet Business Server) 协议是卡内基-梅隆大学开发的电子商务协议。到目前为止，还没有文献对IBS协议进行基于符号化模型检测的安全分析。为此，本文首先采用 SMV 符号化模型检测工具对比较简单的智力扑克协议(mental poker)的公平性进行了安全验证。接着对IBS协议的不可否认性、公平性等安全性能进行了验证。结果表明IBS协议不满足不可否认性和公平性。根据检测结果给出的现实攻击路径，我们对协议进行了相应的改进。随后，我们还在有第三方攻击者的安全模型下对IBS协议的安全验证。

关键词：符号化模型检测安全协议有序二叉决策树智力扑克协议

来源：评论

学校读者我要写书评

暂无评论

可能性测度下并发系统的符号化模型检测研究与实现

可能性测度下并发系统的符号化模型检测研究与实现

引用

作者：张延波陕西师范大学

学位级别：硕士

模型检测是一种形式化的自动验证技术。1981年,由Clarke,Emerson,Quielle和Sifakis提出。它的基本思想是:通过状态空间的穷举搜索来验证有穷状态系统上性质的正确性。它不仅可以自动执行,而且能在系统不满足性质时提供反例。但近些年随... 详细信息

模型检测是一种形式化的自动验证技术。1981年,由Clarke,Emerson,Quielle和Sifakis提出。它的基本思想是:通过状态空间的穷举搜索来验证有穷状态系统上性质的正确性。它不仅可以自动执行,而且能在系统不满足性质时提供反例。但近些年随着系统复杂性的增加,系统中不确定信息亟待处理,且状态爆炸问题也越来越严峻,现有的模型检测技术已经不能完全适用于复杂系统的验证。因此,对模型检测技术进行扩展是重要的也是必要的。目前,国内外学者在经典的模型检测和概率模型检测领域对符号化模型检测做出了大量的研究,但对于可能性测度下的模型检测却没有相应的符号化研究。本文对可能性测度下符号化模型检测进行了研究,是对可能性测度下的模型检测技术和符号化模型检测技术的扩展,对于复杂系统的模型检测的实现与推广具有一定的意义。本文研究了可能性测度下并发系统的符号化模型检测,并设计了一个可能性测度下的符号模型检测器。一方面处理了复杂系统验证中的不确定信息,另一方面缓解了复杂系统验证中的状态爆炸问题。本文研究内容主要分为以下几点:(1)提出可能性测度下并发系统的符号化模型。当并发系统的状态较多时,符号化模型可以较好的表示系统状态及状态之间的迁移关系,以减少存储空间和提高验证效率。(2)研究了可能性测度下的符号化模型检测算法。将系统模型和状态利用多终端二叉树进行符号化表达,并且利用不动点技术实现了验证算法。(3)基于NuSMV的基础,研究并设计了一个可能性测度下的符号化模型检测器,给出了可能性测度下的模型检测器的实现方案,探讨了该模型检测器的实现方法。研究意义主要有:补充了可能性测度下并发系统的符号化模型检测理论,给出了可能性测度下的模型检测器的实现方案,为可能性测度下并发系统检测的推广奠定了基础。

关键词：模型检测可能性测度符号化模型检测并发系统 NuSMV

来源：评论

学校读者我要写书评

暂无评论

基于时态测试器的实时分支时态逻辑模型检测

引用

软件学报 2022年第8期33卷 2930-2946页

作者：骆翔宇黄欣玥古天龙苏开乐陈祖希郑黎晓华侨大学计算机科学与技术学院福建厦门361021 广西可信软件重点实验室(桂林电子科技大学) 广西桂林541004 暨南大学信息科学技术学院/网络空间安全学院广东广州510632 南京信息工程大学人工智能学院江苏南京210044

基于自动机理论的模型检测技术在形式化验证领域处于核心地位,然而传统自动机在时态算子上不具备可组合性,导致各种时态逻辑的模型检测算法不能有机整合.为了实现集成限界时态算子的实时分支时态逻辑RTCTL*的高效模型检测,提出一种RTCTL... 详细信息

基于自动机理论的模型检测技术在形式化验证领域处于核心地位,然而传统自动机在时态算子上不具备可组合性,导致各种时态逻辑的模型检测算法不能有机整合.为了实现集成限界时态算子的实时分支时态逻辑RTCTL*的高效模型检测,提出一种RTCTL*正时态测试器构造方法以及相关符号化模型检测算法,既证明了所提出的RTCTL*正时态测试器构造方法是完备的,也证明了该算法时间复杂度与被验证系统呈线性关系,与公式长度呈指数关系.基于JavaBDD软件包成功开发了该算法的模型检测工具MCTK2.0.0.完成了MCTK与著名的符号化模型检测工具nu Xmv之间的实验对比分析工作,结果表明:MCTK虽然在内存消耗上要多于nu Xmv,但是MCTK的时间复杂度双指数级小于nuXmv,使得利用MCTK验证大规模系统的实时时态性质成为可能.

关键词：符号化模型检测公平离散系统正时态测试器实时分支时态逻辑二元决策图

来源：评论

学校读者我要写书评

暂无评论

离散实时时态认知逻辑的符号化反例生成

离散实时时态认知逻辑的符号化反例生成

引用

作者：梁森华侨大学

学位级别：硕士

模型检测最重要的特性之一是能够为不满足的时态属性生成反例。反例可以为工程师提供调试信息,以进一步解释属性的违反情况。然而,在模型检测的发展中,迄今为止对反例的研究依然很少。已有的最先进的符号化模型检测工具在规范描述上表... 详细信息

模型检测最重要的特性之一是能够为不满足的时态属性生成反例。反例可以为工程师提供调试信息,以进一步解释属性的违反情况。然而,在模型检测的发展中,迄今为止对反例的研究依然很少。已有的最先进的符号化模型检测工具在规范描述上表达力不足,仅能验证实时时态认知逻辑的小部分子集,而且产生的反例相对简单、不完整、并且缺乏便于理解的注释。为此,本文首次提出了一种新的实时分支时态认知逻辑RTCTLK,它是计算树逻辑CTL结合了实时区间和认知的扩展,使得实时相关性质、智能体认知状态及两者共同作用下,即某时间区间内智能体的认知可达关系可以被方便地描述和验证。然后我们给出了基于测试器的符号化反例生成算法,深度改进并实现了新的模型检测工具,使其能够自动为RTCTLK生成足够简洁的图形化反例,更易于直观分析。本文主要研究工作包括定义RTCTLK的语法语义,给出反例生成算法并实现符号化模型检测工具—MCTK2,具体如下:(1)我们定义了表达能力更强的实时分支时态认知逻辑RTCTLK,它是CTL的一个扩展,同时具有离散的时间区间和认知逻辑。(2)基于公平性离散系统JDS,我们设计了RTCTLK的反例生成算法。生成的反例是具有分支结构的有向状态迁移图。为便于理解,在图中的状态和迁移关系上附有一些满足的子公式来加以注释,每个强连通的分量都是一个循环,对应的分量图是树状结构。而且,为避免产生庞大的树状模型图,子公式的证据将依据用户需要而交互式产生。由于图上每个节点均是可交互的,对于附加在状态上的每个未解释的子公式(前面含有路径量词或认知算子),当用户单击该状态时,从当前状态会创建出新的分支。而且对于JDS上RTCTLK的全称片段,我们证明了其反例生成算法的完备性。(3)开发了一个符号化模型检测工具MCTK2,并实现了RTCTLK的反例生成算法。通过与著名的模型检验器nuXmv和MCMAS进行一系列实验比较,分析结果表明,相比于nuXmv,MCTK2在验证RTLTL公式并产生反例的时间效率上优于nuXmv,在易用性以及验证CTLK、RTLTL、RTCTL公式并产生反例的时间消耗和内存占用方面均优于MCMAS。

关键词：符号化模型检测 RTCTL*K 反例生成 MCTK2

来源：评论

学校读者我要写书评

暂无评论

基于UPPAAL的认知机器人控制行为建模与验证

引用

小型微型计算机系统 2016年第6期37卷 1279-1283页

作者：巩卫卫王瑞李晓娟首都师范大学高可靠嵌入式系统技术北京市工程研究中心电子系统可靠性重点实验室北京100048

随着机器人技术的高速发展,越来越多的人开始聚焦到认知机器人领域的研究,机器人系统中的两大研究领域主要是路径规划和任务规划,而传统的规划问题主要侧重于任务规划.本文的研究是在机器人基于行为的控制结构的基础上,提出机器人系统... 详细信息

随着机器人技术的高速发展,越来越多的人开始聚焦到认知机器人领域的研究,机器人系统中的两大研究领域主要是路径规划和任务规划,而传统的规划问题主要侧重于任务规划.本文的研究是在机器人基于行为的控制结构的基础上,提出机器人系统的任务规划层次框架.认知机器人的大部分的控制行为需要人的参与,这就要求这类机器人系统具有在线自适应的能力,而采用传统的验证方法验证其正确性和实时性上存在一定的局限性.采用形式化方法对认知机器人系统的简单实例建模并验证几个重要的属性,采用时间自动机对系统进行形式化的描述,并结合符号化模型检测工具Uppaal进行验证.针对系统的重要属性采用计算树逻辑的形式表述.

关键词：认知机器人系统行为验证符号化模型检测 Uppaal

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：