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

作者：张秀玲暨南大学

学位级别：硕士

分布式系统是计算机科学中十分重要的一个研究领域。随着现代计算机集群规模的不断增长，所处理的数据量越来越大，越来越多的数据库系统通过数据库副本或数据分区的方式提供可拓展的数据存储与服务。在分布式多副本系统中，网络通信和... 详细信息

分布式系统是计算机科学中十分重要的一个研究领域。随着现代计算机集群规模的不断增长，所处理的数据量越来越大，越来越多的数据库系统通过数据库副本或数据分区的方式提供可拓展的数据存储与服务。在分布式多副本系统中，网络通信和节点运行状况的不可控性是实现副本一致性面临的主要障碍。随着分布式副本一致在实际中的应用越来越广泛，集群所处的网络状况和节点运行状况的复杂度急剧上升，分布式一致性问题变得日益重要。　　Paxos算法作为最经典的一致性算法，解决的问题是一个分布式系统如何就某个值(决议)达成一致。Paxos可以应用在数据复制、命名服务、配置管理、权限设置和号码分配等场合，是解决分布式一致性问题最有效的算法之一。　　分布式一致性算法由于本身的高并发性而难以保证其正确性，并且在具体实现时难以调试。因此对分布式一致算法的验证通常采用模型检测的方法。本文通过对应用最广泛的Paxos算法进行建模验证，对模型优化以减少搜索空间，对算法的安全性(Safety)和存活性(Liveness)属性进行了验证，建立的模型相比其他学者所做的模型更具友好型和实用性。　　本文工作主要涉及三个方面：(1)对几种常见的分布式一致性算法的工作原理，交互规则及其应用进行了汇总性研究。(2)按照理论描述用Promela对ClassicPaxos和FastPaxos进行建模。(3)通过Spin工具进行验证。在穷举了所有状态的情况下，验证算法的正确性，确保算法的安全性和存活性要求。　　本文的主要贡献：　　(1)完善了Paxos模型检测内容：本文建立了基于协调者(Coordinator)的ClassicPaxos算法和FastPaxos算法的模型，相对之前学者所做的模型更贴近实现且易于理解，验证的算法是现实中最常用的ClassicPaxos和FastPaxos，完善了对Paxos算法的模型检测。　　(2)在安全性的基础上实现了对存活性的验证：根据分布式领域中的CAP定理，一致性和可用性是衡量一个分布式算法的重要属性，本文在验证安全性属性的同时，还引入线性时态逻辑去验证了存活性属性，验证了算法在保证一致性的同时还具有可用性。

关键词：模型检测技术 Paxos验证分布式系统线性时态逻辑安全性属性

来源：评论

学校读者我要写书评

暂无评论

基于模型检测技术的工控协议漏洞挖掘系统研究

引用

河南科技 2018年第4期37卷 41-42页

作者：王捷李晶田里国网湖北省电力有限公司电力科学研究院湖北武汉430077 国网湖北省电力有限公司湖北武汉430077 国网湖北省电力有限公司十堰供电公司湖北十堰442000

针对工控协议漏洞挖掘技术存在适应差、命中率低等问题,本文采用模型检测技术,对工控协议漏洞挖掘系统的实现进行了设计研究.研究得出：该系统主要由代码的预处理、代码的转化、模型检测阶段组成.希望本文的研究能为学者提供借鉴.

关键词：模型检测技术漏洞挖掘预处理代码的转化模型检测

来源：评论

学校读者我要写书评

暂无评论

模型检测技术的发展研究

引用

科学家 2016年第10期4卷 19-,22页

作者：杨茜茜西南交通大学

模型检测(model checking)是一种能够自动验证有限状态并发系统的技术。该文从模型检测技术的背景入手,先阐述了模型检测技术基本原理及其相关过程。而后介绍了阻碍模型检测技术发展的状态爆炸问题,再者对Nu SMV、SPIN和UPPAAL等模型检... 详细信息

模型检测(model checking)是一种能够自动验证有限状态并发系统的技术。该文从模型检测技术的背景入手,先阐述了模型检测技术基本原理及其相关过程。而后介绍了阻碍模型检测技术发展的状态爆炸问题,再者对Nu SMV、SPIN和UPPAAL等模型检测工具进行了介绍与比较。最后总结了模型检测技术在新的领域、工具研制、算法研究和与其他技术相结合等几个方面的研究进展,可为今后进一步对计算机硬件、通信协议、控制系统、安全认证协议等方面的分析与验证中提供借鉴。

关键词：模型检测技术形式化验证状态爆炸状态约简研究进展

来源：评论

学校读者我要写书评

暂无评论

数据高真实性的车联网Gatekeeper+协议研究及验证

引用

计算机应用与软件 2024年第7期41卷 115-120页

作者：陈肜心陈世超刘杰杨佳北京交通大学电子与信息工程学院北京100044 南华大学计算机学院湖南衡阳421001

车联网通信中数据包的真实性直接关系到车联网通信的安全性。新型车载广播认证协议Gatekeeper具有源身份认证和防护DoS攻击的优势,将是未来主流的车联网通信协议之一。但目前其缺乏对数据真实性的保障机制,导致车载通信会因数据真实性... 详细信息

车联网通信中数据包的真实性直接关系到车联网通信的安全性。新型车载广播认证协议Gatekeeper具有源身份认证和防护DoS攻击的优势,将是未来主流的车联网通信协议之一。但目前其缺乏对数据真实性的保障机制,导致车载通信会因数据真实性的缺失破坏通信的完整性、鲁棒性和安全性。因此,在原协议的通信中建立多重反馈机制,增加对数据真实性的认证方法,扩展成Gatekeeper+协议,弥补对数据真实性保障机制上的不足。并使用时序逻辑CTL建立数据真实性的逻辑表达式,通过模型检测技术验证了Gatekeeper+协议在通信中数据真实性保障能力,还进一步验证了扩展后Gatekeeper+协议的安全性和完整性,确保新协议在车载通信服务中的安全可靠。

关键词：车联网 Gatekeeper+协议数据真实性模型检测技术

来源：评论

学校读者我要写书评

暂无评论

基于模型检测的企业财务造假识别研究

基于模型检测的企业财务造假识别研究

引用

作者：向泊妍南京理工大学

学位级别：硕士

中国股市从1989年试点开始,至今已经历时40年。在此期间,上市公司数量和总体规模增长迅速,为我国经济发展注入了强劲动力。但是由于我国证券市场发展时间较短,相关监管制度不够完善等原因,导致各上市公司披露财务数据时,仍出现大量造假... 详细信息

中国股市从1989年试点开始,至今已经历时40年。在此期间,上市公司数量和总体规模增长迅速,为我国经济发展注入了强劲动力。但是由于我国证券市场发展时间较短,相关监管制度不够完善等原因,导致各上市公司披露财务数据时,仍出现大量造假的情况。不仅直接损害投资者的利益,更长远地对中国证券市场发展产生负面影响。因此,如何利用科技的手段,高效的对各上市公司纰漏的财务数据进行精准分析,识别财务造假手段,同时达到预警的目的已经成为监管层和投资者共同的需求。现有的检测措施主要是依靠监管层人工处理,对财务报表中一些项目的数据、分类、提供方式或披露方式进行操纵、伪造或更改的行为进行识别,导致排查造假信息困难且效率低下,所以一套自动化、准确度高的财务造假检测方法显得尤为重要。模型检测技术是一种基于模型的、自动的性质验证方式,通过对状态空间的穷尽搜索来检查某个系统的行为是否满足某些性质。如果将公司各项财务指标的变化抽象为模型,用来映射公司的状态,通过找出这些状态之间的关系路径,观察该路径最终是否达到某一事件节点,即可以判断该公司的财务信息是否是正确,进而得出信息是否真实。本文基于模型检测方法构建财务造假检测模型,并结合中国市场案例进行实证研究,主要以虚构收入、利润类财务造假为切入点,其性质恶劣、造假方式典型。本文利用2000年至2018年1月期间A股上市企业财务造假违规信息数据进行建模,并对模型检测技术判别的准确性进行了验证。在对这批A股上市公司违规数据的造假特征分析的基础上提取财务指标特征值,利用随机森林进行特征重要性评估,形成财务造假初始判别路径;根据初始规则所需的指标,对造假状态序列进行建模,进行财务造假过程分析并对检测结果进行具体案例验证,形成有价值的财务造假识别模型,结果证明能够预测未来发生造假的可能性,验证了模型检测方法对上市公司财务造假进行识别的可行性。在理论和方法研究价值上,本文为监管机构提供财务造假提供新的研究路径;在实践应用价值上,本文为相关利益方快速识别财务报表中数据造假提供可操作模型和方法。

关键词：财务造假模型检测技术财务指标 Themis异常值分析

来源：评论

学校读者我要写书评

暂无评论

基于模型检测的财经舆情可信度研究

基于模型检测的财经舆情可信度研究

引用

作者：张叙南京理工大学

学位级别：硕士

互联网高速发展,舆情的影响力愈发强烈。民众对于舆情信赖的程度所表现的态度即是舆情可信度,而财经舆情即指有关经济活动的舆情。财经舆情立足于国民经济系统运行的各个方面,财经舆情影响着一般民众和投资者的态度与行为,而财经领域的... 详细信息

互联网高速发展,舆情的影响力愈发强烈。民众对于舆情信赖的程度所表现的态度即是舆情可信度,而财经舆情即指有关经济活动的舆情。财经舆情立足于国民经济系统运行的各个方面,财经舆情影响着一般民众和投资者的态度与行为,而财经领域的调查性报道、股市类报道、预测性报道、政策解读类报道和投资理财类报道满足了受众信息需求的同时,其虚假舆情也对社会经济系统产生了不可估量的负面影响,尤其是在涉及资本市场的相关舆情,损害了上市公司及投资者的合法权益。为了应对虚假财经舆情,除加强舆情的法律和制度发展外,学者研究了技术手段监测和干预。如面向以网络财经舆情为主的虚假财经舆情快速检测系统和降低高影响力财经舆情扩散范围的有效抑制算法。然而这些方法仍存在一些问题,诸如对一定空间内数据处理量有限、未能建立统一标准的数据规则进行可信度检测、没能融入自然语言处理、检测自动化程度低等问题,因此设计一套高效率、高准确率的检测框架具有极强的社会意义。从已有的研究可知,财经舆情的发生伴随着企业财务、非财务以及舆情指标的变化,因此关联分析各项指标的波动同样可以反映舆情事件发展的过程,因此可以根据企业财务、非财务以及舆情指标状态改变路径的正确与否来判断舆情是否可信,将舆情状态变化转化为规则模型,通过对规则模型进行检测来验证状态的变化是否正确合理,从而判断舆情是否可信。模型检测是一种用来检验复杂系统时序逻辑关系正确性和可靠性的自动验证方法,若通过将财经舆情状态转移关系模型化,通过模型检测验证该模型是否正确并可以起到舆情检测作用,用以验证舆情是否可信。本论文针对财经舆情的状态特征以及模型检测技术的特点进行框架设计,形成一套完整的财经舆情检测系统:首先对舆情进行状态提取,针对财务指标、非财务指标、舆情指标等抽取出状态实体,根据时序关系形成状态转移关系,最终形成待检测的路径模型。其次,采集金融事件案例数据,抽取出检验规则,形成检测规则库。最后通过对舆情状态转移关系的模型检测来验证舆情是否可信。通过实验表明,该系统可以有效检测财经舆情可信度,同时为时序关系下的舆情可信度检测提供了理论支撑。

关键词：财经舆情可信度检测模型检测技术状态转移关系

来源：评论

学校读者我要写书评

暂无评论

基于线性时态逻辑的模型检测技术研究

基于线性时态逻辑的模型检测技术研究

引用

本项目对基于线性时态逻辑的模型检测技术进行了深入研究，解决的主要技术问题包括：提出了基于线性时态逻辑模型检测和有限状态自动机模型的测试例生成优化技术；针对模型检测技术应用中所存在的状态爆炸问题，提出了一种模块化线性时... 详细信息

标准号: gkls127914

本项目对基于线性时态逻辑的模型检测技术进行了深入研究，解决的主要技术问题包括：提出了基于线性时态逻辑模型检测和有限状态自动机模型的测试例生成优化技术；针对模型检测技术应用中所存在的状态爆炸问题，提出了一种模块化线性时态逻辑模型检测方法；提出了面向测试序列生成的自动机建模/导出/转换方法；研发了一套面向应用的可视化模型检测工具。　　本项目主要技术性能指标如下：　　1、所提出的基于线性时态逻辑模型检测和有限状态自动机模型的测试例生成技术，能有效地生成高质量的测试例；　　2、所提出的模块化线性时态逻辑模型检测方法能有效克服状态爆炸问题；　　3、所提出的面向测试序列生成的状态自动机转换方法能面向测试例生成，将扩展有限状态自动机模型转换为较为简单的有限状态自动机模型；　　4、所研发的可视化模型检测工具性能良好，功能齐全，可方便用户掌握并使用模型检测技术。　　本项目的研究成果应用领域非常广泛，在通讯协议、硬件设计、工业控制逻辑领域、软件测试等领域均有成功的使用案例。经过20多年的发展，我国已形成了规模庞大的计算机产业体系。可以预料本项目研究成果从长期来看存在广阔的市场需求，具有良好的产业化潜力。

关键词：线性时态逻辑模型检测技术有限状态状态爆炸

来源：评论

学校读者我要写书评

暂无评论

基于模型检测的多处理器实时系统可调度性自动化分析

引用

现代计算机（中旬刊） 2017年第1期 20-24页

作者：杜伊四川大学计算机学院成都610065

近年来,模型检测技术获得快速的发展,已有学者将模型检测技术用于多处理器实时系统可调度性分析。但如果对每个实际系统都手工建立模型进行可调度性验证,过程繁琐且模型不可重复利用。针对此,开发一个工具用于自动完成可调度性检测,并... 详细信息

近年来,模型检测技术获得快速的发展,已有学者将模型检测技术用于多处理器实时系统可调度性分析。但如果对每个实际系统都手工建立模型进行可调度性验证,过程繁琐且模型不可重复利用。针对此,开发一个工具用于自动完成可调度性检测,并可视化显示结果。

关键词：模型检测技术多处理器实时系统可调度性自动化可视化

来源：评论

学校读者我要写书评

暂无评论

基于模型检测技术的NS协议分析模型的研究

基于模型检测技术的NS协议分析模型的研究

引用

作者：姚军电子科技大学

学位级别：硕士

计算机技术迅速发展,并且越来越多的渗透到各个行业和领域。尤为重要的是人们对软件的可靠性要求也越来越高。为了提高软件可靠性,众多专家学者对多种方法进行了研究。在众多的理论和方法中,模型检测(model checking)成为近几年的研究... 详细信息

计算机技术迅速发展,并且越来越多的渗透到各个行业和领域。尤为重要的是人们对软件的可靠性要求也越来越高。为了提高软件可靠性,众多专家学者对多种方法进行了研究。在众多的理论和方法中,模型检测(model checking)成为近几年的研究热点。基于该理论的研究,在高可靠性的软件设计领域也不断取得了重大的应用。　　模型检测是一种形式化验证方法,它将需要验证的系统抽象成有限状态模型,并使用时序逻辑语言描述系统所要检测的属性,然后对以上抽象出的模型进行有限状态的穷尽搜索。使用模型检测技术对电子商务协议进行分析建模并且验证其安全性是近年来的研究热点。　　本文详细地介绍了模型检测的理论背景,以及现在使用较为广泛的模型检测工具,例如SPIN,SMV等等。其中,SPIN是由贝尔实验室开发的一种模型检测工具,用于分析软件系统的设计模型和各种协议的设计模型。同时,模型检测在电子商务协议中的应用也进行了介绍。以及,对 Needham-Schroeder公钥密码协议进行了说明。　　在进行验证时,使用了模型检测工具 SPIN对 NS协议进行分析。首先使用该工具的语言 promela描述协议模型。其次,时序逻辑语言 LTL规约了待测属性,最后SPIN验证后得到验证结果。在对协议模型的检测结果进行分析时,发现了植入的协议漏洞,得出了协议的攻击路径。从而进一步证明了该协议必须要满足的认证性和秘密性。

关键词：模型检测技术 SPIN软件电子商务协议 NS协议

来源：评论

学校读者我要写书评

暂无评论

安全协议的Rubin逻辑及有色Petri网分析方法研究与应用

安全协议的Rubin逻辑及有色Petri网分析方法研究与应用

引用

作者：徐洋贵州大学

学位级别：博士

当今，随着网络技术的迅猛发展和广泛应用，网络已经成为人们共享信息的主要方式，人们可以随时、随地以各种方式提供和接受信息。然而，网络技术是一把双刃剑，在给人们带来巨大便利的同时也给信息的安全造成巨大威胁。因此，在当今信... 详细信息

当今，随着网络技术的迅猛发展和广泛应用，网络已经成为人们共享信息的主要方式，人们可以随时、随地以各种方式提供和接受信息。然而，网络技术是一把双刃剑，在给人们带来巨大便利的同时也给信息的安全造成巨大威胁。因此，在当今信息社会，信息安全的重要性与日俱增。而作为网络通信基础的安全协议是通信各方的桥梁。由此可见，协议安全是信息安全领域的重要课题。\n 然而，设计一个健壮有效的安全协议非常困难，这不仅因为网络的复杂性还因为安全协议的多目标性。实践证明，设计和分析安全协议需要依靠形式化方法和理论。经过20多年的研究和发展，在安全协议的形式化方法和理论领域，百家争鸣，百花齐放。但是，现有的形式化理论和方法都不完善。因此，深入研究安全协议的形式化分析理论和方法意义重大。\n 安全协议的形式化分析方法主要分为三类：基于推理结构的方法，又称形式逻辑方法，基于攻击结构的方法，又称模型检测方法，基于证明结构的方法。基于逻辑的形式化方法是最直接也是最简单的方法，已经被广泛研究和应用。Rubin博士提出的Rubin逻辑是第一个可以推理非单调协议的逻辑。与BAN类逻辑相比，Rubin逻辑有诸多优点。可以说，Rubin逻辑是安全协议分析中一个有潜力、有前途的方法。模型检测技术一般使用自动化工具，在自动程度方面表现良好。属于高级Petri网的有色Petri网已经被证明是一个适于安全协议建模的方法。尽管如此，使用有色Petri网分析安全协议仍然需要进一步研究。\n 本文主要对安全协议的Rubin逻辑的形式化方法与基于有色Petri网的模型检测技术进行了深入研究，我们还系统研究了这两种方法在协议形式化分析中的应用。我们对Rubin逻辑进行了一系列扩展和改进。此外，我们还提出了两种基于有色Petri网的协议分析新方法。我们采用上述新方法分析了多个安全协议。总的来讲，从理论和实践两个层面上研究了安全协议的形式化分析。主要工作有以下几个方面：\n 1.对安全协议的基本理论进行了研究，介绍了安全协议的基本概念，给出了一个安全协议模型，分析了安全协议的基本性质。指出了安全协议分析的复杂性。并着重对目前的安全协议分析形式化方法进行了分析和讨论。\n 2.研究了基于逻辑的安全协议形式化分析方法，其中对ZQ逻辑和Rubin逻辑进行了着重的研究。介绍了BAN逻辑及其两个重要扩展GNY逻辑和SVO逻辑。提出了一个新的可追究和公平协议，这个协议是ISI支付协议的一个改进版本，并用ZQ逻辑分析了新的协议满足追究性和公平性。此外，应用Rubin逻辑分析了Andrew安全RPC协议及其两个改进协议，发现原始协议存在已知漏洞，并且发现***修改后的协议仍然存在漏洞，随后，提出了一个新的改进，克服了所发现的漏洞。还应用Rubin逻辑分析了SSL协议的恢复一个已存在的会话模式。此类实用协议往往难以用BAN类逻辑来分析。分析发现，此模式下SSL协议能够实现建立新的安全连接的目标。这两个例子说明Rubin逻辑能够较好的克服BAN类逻辑的缺陷。\n 3.着重研究了如何扩展Rubin逻辑，并提出了三个扩展。研究发现Rubin逻辑难以分析含有时间戳的消息，此外，Rubin逻辑不适用于分析非否认性、可追究性及公平性，而这三个性质都是电子商务协议强调的安全性质。由此，提出对Rubin逻辑的三个扩展。第一个扩展可用于分析含有时间戳的消息。采用ZQ逻辑的思想提出了第二个扩展，可用于分析非否认性。第三个扩展是在第二个基础上进行的，可以分析非否认性、可追究性和公平性，阐述了如何应用改进后的方法对电子商务协议进行分析。这三个扩展彼此联系，可以根据协议类型不同灵活使用。\n 另一方面，采用扩展后的Rubin逻辑对三个分属不同类型的安全协议进行了分析。分析了采用时间戳的X.509认证协议，发现协议不仅不能实现它的三个目标而且还存在冗余。随后给出了两个改进，其中一个改进没用使用时间戳。此外，分析了MANET中一个安全路由协议——ARAN，尤其，分析了协议中证书废除这种非单调的知识。发现了该协议存在的一些问题，并提出一个改进。还分析了Zhou-Gollman协议这一经典的电子商务协议。与其他方法不同之处在于，不仅分析了该协议的可追究性和公平性，还分析了其机密性，完整性和新鲜性。发现该协议可以满足完整性，但是不能实现机密性，交易双方也很难确定消息的新鲜性。实例分析表明，扩展后的Rubin逻辑不论在分析认证协议还是分析电子商务协议中都表现良好。\n 4.研究了有色Petri网的基本理论及其一个自动化工具CPNTools。阐述了Petri网及有色Petri网的形式化定义。分析讨论了有色Petri网的动态特性。此外对CPNTools的应用接口及如何使用这一工具对有色Petri网进行建

关键词：安全协议 Rubin逻辑有色Petri网模型检测技术

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：