检索结果-南通市图书馆

在线全文

学校读者我要写书评

暂无评论

多Web服务组合兼容性的自动化验证

计算机工程与应用 2016年第7期52卷 67-73页

作者：贾志淳邢星渤海大学信息科学与技术学院辽宁锦州121013 哈尔滨工业大学航天学院哈尔滨150001

Web服务组合的目的是实现单一服务无法满足的复杂功能,而保证组合的正确性以实现服务增值是十分必要,因此组合之后的正确性验证是Web服务组合的一个重要研究方向。从Web服务交互行为方面描述多Web服务组合,在提出行为兼容性的相关理论... 详细信息

Web服务组合的目的是实现单一服务无法满足的复杂功能,而保证组合的正确性以实现服务增值是十分必要,因此组合之后的正确性验证是Web服务组合的一个重要研究方向。从Web服务交互行为方面描述多Web服务组合,在提出行为兼容性的相关理论的基础上,给出基于Pi演算的多Web服务组合行为兼容性的自动化验证算法,通过将多Web服务组合自动转化为Pi演算中的组合进程,实现多Web服务组合的自动化验证。

关键词： Pi演算 Web服务组合行为兼容性 Web服务行为自动化验证

算法的形式化推导与基于Isabelle的自动化验证

在线全文

学校读者我要写书评

暂无评论

江西师范大学学报（自然科学版） 2018年第4期42卷 379-383页

作者：齐蕾蕾杨庆红游颖江西师范大学计算机信息工程学院江西南昌330022

可信软件的不断发展进一步推动了形式化方法的深入研究.结合实际应用中的2个问题,采用基于递推关系的算法形式化方法,演示了算法的形式化推导过程,并运用Isabelle定理证明器结合Dijkstra最弱前置谓词方法,对得到的算法程序进行了自动化... 详细信息

可信软件的不断发展进一步推动了形式化方法的深入研究.结合实际应用中的2个问题,采用基于递推关系的算法形式化方法,演示了算法的形式化推导过程,并运用Isabelle定理证明器结合Dijkstra最弱前置谓词方法,对得到的算法程序进行了自动化验证,避免了手工验证过程繁琐和易出错等问题.研究表明:基于递推关系的算法形式化方法不仅可以提高开发算法的效率,而且通过数学变换保证推导过程的正确性,从而有效保证了算法和程序的正确性.

关键词：形式化方法 Isabelle定理证明器自动化验证形式化推导

改进Athena算法的多协议攻击自动化验证方法

在线全文

学校读者我要写书评

暂无评论

计算机科学 2014年第12期41卷 112-117,132页

作者：刘威郭渊博雷新锋李俊锋解放军信息工程大学数学工程与先进计算国家重点实验室中国人民解放军第61840部队太原卫星发射中心

多协议环境下协议安全性问题是安全协议形式化分析验证领域的一个公开问题。针对此问题,在分析Athena算法的基础上提出了一种多协议攻击自动化验证方法。该方法扩展了Athena状态表示方法和后继状态生成算法,使得攻击者具备截取其它协议... 详细信息

多协议环境下协议安全性问题是安全协议形式化分析验证领域的一个公开问题。针对此问题,在分析Athena算法的基础上提出了一种多协议攻击自动化验证方法。该方法扩展了Athena状态表示方法和后继状态生成算法,使得攻击者具备截取其它协议交互消息和计算生成当前协议消息的能力,能够以自动化的方式验证协议是否存在多协议攻击。实验结果表明,提出的方法能够实现多协议攻击的自动化验证。

关键词：多协议攻击自动化验证安全属性 Athena算法逆向搜索

SET证书申请协议在SPV下的自动化验证及改进

在线全文

学校读者我要写书评

暂无评论

计算机学报 2008年第6期31卷 1035-1045页

作者：肖茵茵苏开乐岳伟亚陈清亮吕关锋杨晋吉中山大学信息科学与技术学院广东省信息安全重点实验室广州510275 暨南大学计算机科学系广州510632 北京工业大学计算机学院北京100022

基于实例化空间逻辑理论,使用知识推理方法,在SPV(Security Protocol Verifier)下对完整SET证书申请协议的秘密性、认证性等安全性质进行了完全自动化证明,并对协议进行了改进.SPV调用工业级SAT求解器,能够高效验证安全协议是否满足CAPS... 详细信息

基于实例化空间逻辑理论,使用知识推理方法,在SPV(Security Protocol Verifier)下对完整SET证书申请协议的秘密性、认证性等安全性质进行了完全自动化证明,并对协议进行了改进.SPV调用工业级SAT求解器,能够高效验证安全协议是否满足CAPSL(Common Authentication Protocol Specification Language)协议规范及单层、多层认知规范.应用一个逻辑或工具对协议进行验证首先必须对该协议进行简化,而SET协议作为当前最复杂的工业级协议,其原始文档有上千页,因此简化过程相当困难,相关研究较少,已有的一些简化模型也不够完整.因此,文章针对SET证书申请协议,给出了比以往更贴近原协议的简化模型,并详细阐述了该模型在SPV下的形式化描述及验证过程、验证结果,分析了由于协议不满足某些认知规范所带来的安全隐患,从而对协议进行改进,最后证明了改进后协议的有效性.该工作也充分说明了SPV足以处理复杂的工业级协议.

关键词： SET证书申请协议自动化验证 SPV 认证性秘密性

算法的形式化推导与基于Isabelle的自动化验证

在线全文

学校读者我要写书评

暂无评论

算法的形式化推导与基于Isabelle的自动化验证

作者：齐蕾蕾江西师范大学

学位级别：硕士

可信软件的不断发展,进一步推动了形式化方法的深入研究。形式化方法具有严格的数学语言和精确的逻辑语义,从而保证软件在开发过程中的正确性。形式化方法主要包括形式化推导和形式化验证两个部分。形式化推导是通过对问题程序规约进行... 详细信息

可信软件的不断发展,进一步推动了形式化方法的深入研究。形式化方法具有严格的数学语言和精确的逻辑语义,从而保证软件在开发过程中的正确性。形式化方法主要包括形式化推导和形式化验证两个部分。形式化推导是通过对问题程序规约进行精确变换,最终得到算法程序。形式化验证是在对软件进行规约的基础上,验证软件是否具有所期望的性质。形式化方法对保证软件正确性和可靠性具有十分重要的意义。本文从形式化推导和自动化验证两方面研究提高算法程序正确性的有效途径。在形式化推导方面,采用基于递推技术的算法形式化方法开发算法程序,通过程序规约变换技术对形式化程序规约进行等价变换,得到问题求解的递推关系和循环不变式,以此为基础得到算法程序。该方法不仅清晰地展示了算法的设计思路与过程,而且有效保证了算法程序的正确性。在自动化验证方面,选择Isabelle定理证明器为工具。Isabelle传统应用领域为数学定理证明,本文结合验证需要在对其内置类型库和规则库进行扩充的基础上,探索将它应用于算法程序自动化验证以及问题求解序列递推关系自动化验证的有效方法。论文从三个层面深入剖析了Isabelle定理证明器,从三个部分展示了Isabelle的理论证明过程。结合本文两方面验证工作的需要,对Isabelle的类型库和规则库进行了扩充,完成了新添加规则的内部形式转换和正确性验证,以及新类型的嵌入;然后以此扩充的Isabelle类型库和规则库为基础,采用后推证明方式,结合Dijkstra最弱前置谓词方法,给出了算法程序自动化验证的基本流程,并对若干问题的算法程序进行了自动化验证;同时,为了避免手工推导递推关系带来的人为性错误,基于以上扩充的Isabelle规则库,对本文实例中推导得到的递推关系实现了进一步自动化验证。研究表明,上述工作有效提高了算法程序正确性证明和问题求解序列递推关系正确性验证的效率。

关键词：形式化推导自动化验证递推关系 Isabelle 证明规则库类型库

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

BLP改进模型的形式化描述及自动化验证

计算机工程 2013年第12期39卷 130-135页

作者：徐亮谭煌湖南师范大学数学与计算机科学学院长沙410081 高性能计算与随机信息处理省部共建教育部重点实验室长沙410081

在《信息安全技术操作系统安全技术要求》中,提出访问验证保护级安全操作系统的研发过程需要完全形式化的安全策略模型。针对该情况,对经典的数据机密性BLP模型进行相应改进,为系统中的主客体引入多级安全标签以及安全迁移规则,使其满... 详细信息

在《信息安全技术操作系统安全技术要求》中,提出访问验证保护级安全操作系统的研发过程需要完全形式化的安全策略模型。针对该情况,对经典的数据机密性BLP模型进行相应改进,为系统中的主客体引入多级安全标签以及安全迁移规则,使其满足实际系统开发的需求。运用完全形式化的方法对改进模型的状态、不变量、迁移规则等进行描述,使用Isabelle定理证明器证明了迁移规则对模型的不变量保持性,从而实现对模型正确性的自动形式化验证,并保证了模型的可靠性。

关键词： BLP模型安全策略形式化方法自动化验证定理证明安全操作系统

在线全文

学校读者我要写书评

暂无评论

大型运输机任务管理系统自动化验证

大型运输机任务管理系统自动化验证

集成电路工艺设计包PDK自动化验证与界面化的实现方法

2017年航空智能装备与试验测试技术年会

作者：郭文杰贾鑫航空工业第一飞机设计研究院

针对目前航空电子系统测试过程中出现需求覆盖率低和测试不完整等问题,结合模型驱动的系统设计流程,以设计阶段的UML模型作为验证平台的测试输入,设计了任务管理系统自动化验证平台。并以大型运输机任务管理系统为用例,验证了该平台的... 详细信息

针对目前航空电子系统测试过程中出现需求覆盖率低和测试不完整等问题,结合模型驱动的系统设计流程,以设计阶段的UML模型作为验证平台的测试输入,设计了任务管理系统自动化验证平台。并以大型运输机任务管理系统为用例,验证了该平台的正确性,能够满足型号研制要求。

关键词：任务管理系统模型驱动自动化验证

来源： cnki会议评论

在线全文

cnki会议

学校读者我要写书评

暂无评论

集成电路应用 2019年第8期36卷 17-19页

作者：程长虹孙杰胡少坚上海集成电路研发中心有限公司

分析集成电路的自动化验证PDK方法,以及PDK验证过程中遇到的难点问题。通过Skill汇编语言建立系统化的PDK自动化验证界面工具。这是一套适用于不同工艺,嵌套在Cadence virtuoso平台下的PDK自动化验证方法,可以大大提高PDK验证的质量和... 详细信息

分析集成电路的自动化验证PDK方法,以及PDK验证过程中遇到的难点问题。通过Skill汇编语言建立系统化的PDK自动化验证界面工具。这是一套适用于不同工艺,嵌套在Cadence virtuoso平台下的PDK自动化验证方法,可以大大提高PDK验证的质量和效率。

关键词：集成电路设计工艺设计包自动化验证 Cadence Virtuoso

RTL层次之系统互连线及系统电路的软件自动化验证方法研究

在线全文

学校读者我要写书评

暂无评论

RTL层次之系统互连线及系统电路的软件自动化验证方法研究

作者：陈永光电子科技大学

学位级别：硕士

因为集成电路的复杂度越来越高,只有在流片前保证验证的完整性,IC（Integrated Circuit,集成电路）才有可能一次就流片成功,所以IC验证已经成为了IC设计界的一个极其重要的课题。而因为RTL层次的验证可以更早的发现问题而较少不必要的损... 详细信息

因为集成电路的复杂度越来越高,只有在流片前保证验证的完整性,IC（Integrated Circuit,集成电路）才有可能一次就流片成功,所以IC验证已经成为了IC设计界的一个极其重要的课题。而因为RTL层次的验证可以更早的发现问题而较少不必要的损失,所以其验证方法论就变得更为重要。针对于模块级模块的验证,各家大型EDA工具公司（如Cadence, Synopsys）都提出了非常完善的验证方法论,套用这些验证方法论可以非常全面的验证所有模块而保证模块的功能都没有问题。而一个完整的SoC（System On Chip,片上系统）系统,除了这些经过完整验证的各个模块外,还有很多系统互连线与系统级电路来构成。但针对系统互连线与系统级电路的验证目前还没有成熟的验证方法论,针对这些电路的常用的验证方法效率非常低,极大的影响了IC验证的整体质量,从而使得IC在流片后才发现问题,IC只能改版后再次流片,从而推出市场的时间被大大延后,这样就极大的提高了IC设计的成本并且可能浪费潜在的市场机会。本论文正是针对上述问题,以提高系统互连线与系统级电路的验证完整性为出发点,提出了新的验证方法,而针对验证效率的问题,提出了自动化测试的思路。主要内容为： 1.详细研究了系统互连线与系统级电路的传统验证方法。 2.详细研究了系统互连线与系统级电路的特点,并针对这些特点,提出了描述其电路行为的方法。 3.提出了针对系统互连线与系统级电路的新的验证方法。 4.研究了使用Python语言实现自动化验证的可行性。 5.实现了Python语言自动化测试脚本,可以依据电路行为自动化产生相应的验证环境,并保证测试完整性,极大的提高了测试效率。

关键词：系统互连线系统级电路自动化验证 Python脚本