检索结果-南通市图书馆

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

SOCKET通信程序模型抽取及可靠性验证

计算机科学 2012年第11期39卷 102-105,141页

作者：肖美华余立全肖攀华东交通大学软件学院南昌330013 南昌大学信息工程学院南昌330031 南昌大学软件学院南昌330047

形式化方法是验证并发系统可靠性和安全性的重要手段。对高级语言开发的并发系统自动抽取的模型进行形式化验证是模型检测技术领域中的一个研究热点。鉴于socket函数调用顺序不正确产生的运行时潜在问题(内存泄漏、死锁、边界数据丢失... 详细信息

形式化方法是验证并发系统可靠性和安全性的重要手段。对高级语言开发的并发系统自动抽取的模型进行形式化验证是模型检测技术领域中的一个研究热点。鉴于socket函数调用顺序不正确产生的运行时潜在问题(内存泄漏、死锁、边界数据丢失等),针对顺序结构的socket程序,通过描述Promela消息数据结构和通道,构建socket函数的Promela模型,定义socket函数到Promela映射规则,提出socket函数调用序列抽取算法及目标Promela模型生成算法,用线性时态逻辑(LTL)刻画socket函数调用顺序应满足的性质,开发基于SPIN的socket通信程序分析系统。实验结果表明,该系统能有效检测socket通信程序的运行时潜在问题。

关键词： socket 模型检测模型抽取形式化验证

在线全文

学校读者我要写书评

暂无评论

基于XML的Web应用模型抽取

计算机科学 2011年第9期38卷 130-134,149页

作者：程广金缪淮扣方明科梅佳髙洪皓上海大学计算机工程与科学学院上海200072 上海市计算机软件评测中心上海201112 信阳师范学院计算机与信息技术学院信阳464000

以模型检验为目标,从时间的约束角度出发,提出一种基于XML文档的Web应用的模型抽取方法。模型抽取由时间及相关链接的提取、模型构造和结果显示3部分组成。首先,通过对Web应用进行逆向分析,从带时间约束的XML源代码对链接及时间约束等... 详细信息

以模型检验为目标,从时间的约束角度出发,提出一种基于XML文档的Web应用的模型抽取方法。模型抽取由时间及相关链接的提取、模型构造和结果显示3部分组成。首先,通过对Web应用进行逆向分析,从带时间约束的XML源代码对链接及时间约束等相关信息进行提取、规整和存储。其次,对Web应用中的链接、时间约束等建模元素进行分析,应用映射与聚合等抽象技术对获得的信息进行重构,得到适合于形式化验证的时间自动机(TA,Timed Automata)模型,并对时间约束下的并发进行模型组合。最后,以电子邮箱系统为实例阐述如何实现模型抽取。

关键词： XML文档时间约束模型抽取时间自动机

在线全文

学校读者我要写书评

暂无评论

基于Pro/E二次开发的模型抽取技术

导弹与航天运载技术 2011年第2期 58-61页

作者：张利强刘刚顾翠章翔峰北京神舟航天软件技术有限公司北京100094

为了实现从复杂的装配体中抽取部分零部件进行CAE分析,同时保持被抽取零部件的空间位置关系不变。利用VC2005开发环境和Pro/E自带的Pro/ToolKit开发模块进行二次开发,在Pro/E非可视化的条件下将Pro/E模型导入内存,重新组合生成新装配体... 详细信息

为了实现从复杂的装配体中抽取部分零部件进行CAE分析,同时保持被抽取零部件的空间位置关系不变。利用VC2005开发环境和Pro/E自带的Pro/ToolKit开发模块进行二次开发,在Pro/E非可视化的条件下将Pro/E模型导入内存,重新组合生成新装配体进行实时预览,并将预览合适的新装配体按照指定文件格式保存。结合虚拟火箭案例,验证了复杂模型抽取的可行性和实用性,提高了分析模型抽取、装配的效率和通用性。

关键词： Pro/E模型二次开发 Pro/Toolkit 模型抽取

在线全文

学校读者我要写书评

暂无评论

一种用于模型验证的Web应用模型抽取方法

应用科学学报 2009年第1期27卷 90-96页

作者：方明科缪淮扣上海大学计算机工程与科学学院上海200072 信阳师范学院计算机与信息技术学院河南信阳464000

以模型验证为目标,提出一种Web应用FSM(finite state machines)模型的抽取方法。该方法将模型抽取划分为链接提取、模型构造和结果显示。通过建立标签库和对标签的定位,并结合正则表达式的方法,对Web应用进行逆向分析,从源代码开始进行... 详细信息

以模型验证为目标,提出一种Web应用FSM(finite state machines)模型的抽取方法。该方法将模型抽取划分为链接提取、模型构造和结果显示。通过建立标签库和对标签的定位,并结合正则表达式的方法,对Web应用进行逆向分析,从源代码开始进行链接及相关信息的提取、规整和存储。对Web应用中的页面、链接等建模元素进行分析,应用映射与聚合等抽象技术对获得的信息进行重构,得到适用于验证的Web应用的FSM模型。

关键词：链接提取 Web应用模型模型抽取有限状态机

C2P:基于Pi演算的协议C代码形式化抽象方法和工具

在线全文

学校读者我要写书评

暂无评论

软件学报 2021年第6期32卷 1581-1596页

作者：张协力祝跃飞顾纯祥陈熹数学工程与先进计算国家重点实验室河南郑州450001 网络密码技术河南省重点实验室河南郑州450002

形式化方法为安全协议分析提供了理论工具,但经过形式化验证过的协议标准在转换为具体程序实现时,可能无法满足相应的安全属性.为此,提出了一种检测安全协议代码语义逻辑错误的形式化验证方法.通过将协议C源码自动化抽象为Pi演算模型,基... 详细信息

形式化方法为安全协议分析提供了理论工具,但经过形式化验证过的协议标准在转换为具体程序实现时,可能无法满足相应的安全属性.为此,提出了一种检测安全协议代码语义逻辑错误的形式化验证方法.通过将协议C源码自动化抽象为Pi演算模型,基于Pi演算模型对协议安全属性形式化验证.最后给出了方案转换的正确性证明,并通过对Kerberos协议实例代码验证表明方法的有效性.根据该方案实现了自动化模型抽象工具C2P与成熟的协议验证工具ProVerif结合,能够为协议开发者或测试人员检测代码中的语义逻辑错误提供帮助.

关键词：协议实现形式化验证 Pi演算模型抽取 ProVerif

基于计算模型的安全协议Swift语言实施安全性分析

在线全文

学校读者我要写书评

暂无评论

通信学报 2018年第9期39卷 178-190页

作者：孟博何旭东张金丽尧利利鲁金钿中南民族大学计算机科学学院

分析IOS平台上的安全协议Swift语言实施安全性,对保障IOS应用安全具有重要意义。首先对已有安全协议Swift语言实施进行分析,确定Swift语言子集SubSwift,并给出其BNF;其次基于操作语义,建立SubSwift语言到Blanchet演算的映射模型,主要包... 详细信息

分析IOS平台上的安全协议Swift语言实施安全性,对保障IOS应用安全具有重要意义。首先对已有安全协议Swift语言实施进行分析,确定Swift语言子集SubSwift,并给出其BNF;其次基于操作语义,建立SubSwift语言到Blanchet演算的映射模型,主要包含SubSwift语言的语句、类型到Blanchet演算的语句及类型的映射关系与规则;再次根据Sub Swift语言到Blanchet演算的映射模型,提出从安全协议Sub Swift语言实施生成安全协议Blanchet演算实施方法;最后应用Antrl4工具和Java语言开发安全协议Blanchet演算实施生成工具SubSwift2CV,分析OpenID Connect协议、Oauth2.0协议和TLS协议的SubSwift语言实施安全性。

关键词：安全协议实施安全性 Swift语言形式化分析模型抽取

在线全文

学校读者我要写书评

暂无评论

安全协议实施安全性分析综述

山东大学学报（理学版） 2018年第1期53卷 1-18页

作者：孟博鲁金钿王德军何旭东中南民族大学计算机科学学院湖北武汉430074

安全协议是网络空间安全的重要组成部分,安全协议实施是安全协议的最终表现形式。介绍了安全协议实施安全性分析的意义,分别按照三个前提条件:能够获取安全协议客户端实施和安全协议服务器端实施、仅能够获取安全协议客户端实施、不能... 详细信息

安全协议是网络空间安全的重要组成部分,安全协议实施是安全协议的最终表现形式。介绍了安全协议实施安全性分析的意义,分别按照三个前提条件:能够获取安全协议客户端实施和安全协议服务器端实施、仅能够获取安全协议客户端实施、不能获取安全协议客户端与安全协议服务器端实施,并依据安全协议实施安全性分析采用的主要分析方法——程序验证、模型抽取、网络轨迹、指令分析等,对相关研究成果进行归类、分析、比较、总结和讨论。对未来安全协议实施安全性分析的研究方向进行了展望。

关键词：网络空间安全安全协议实施程序验证模型抽取网络轨迹指令分析

基于自然语言理解的事件驱动物联网模型与规约生成

在线全文

学校读者我要写书评

暂无评论

基于自然语言理解的事件驱动物联网模型与规约生成

作者：张时雨南京大学

学位级别：硕士

物联网（Internet Of Things,Io T）如今已深入到个人生活和工业生产的各个方面,智能设备大量出现在家庭生活中,为用户带来舒适和便利。然而由于智能家居系统复杂多变,用户缺乏专业知识等原因,所面临的安全挑战也越来越严峻。智能家居... 详细信息

物联网（Internet Of Things,Io T）如今已深入到个人生活和工业生产的各个方面,智能设备大量出现在家庭生活中,为用户带来舒适和便利。然而由于智能家居系统复杂多变,用户缺乏专业知识等原因,所面临的安全挑战也越来越严峻。智能家居系统与用户的隐私、财产和生命安全息息相关,如何保证其安全性成为相关领域的重要研究课题。模型检验技术是近年来事件驱动物联网系统安全验证中被广泛使用的技术之一。该技术对复杂系统建立状态迁移模型来描述系统行为,通过自动遍历系统模型的有限状态空间来验证系统是否满足某些性质。然而在对真实Io T系统进行验证时,模型检验技术仍然面临一些问题。第一,Io T系统由各种设备组成,对设备准确建模决定了验证结果的可信度。目前设备模型的获取采用人工建模或源码分析的方法,这些方法得到的模型大多与真实设备有差异,很少有研究工作考虑从设备的自然语言文本描述中获取模型。第二,模型检验技术采用形式化规约来描述系统性质,最常用是线性时序逻辑（Linear Temporal Logic,LTL）。但普通用户不具备专业的数理知识,无法理解或提供形式化规约,他们通常使用自然语言来表达需求。这些问题极大地限制了现有验证工具在真实Io T系统上的应用。针对以上两个问题,本文从以下方面展开系统研究:··针对设备建模问题,本文提出了一种基于IFTTT功能描述自然语言处理的设备辅助建模方法。该方法首先利用自然语言处理技术对设备功能描述语句进行分析,抽取出每个句子的语义信息。然后利用词向量技术和语义词典,针对功能描述的特点设计了功能相关性评估策略,通过对功能描述聚类分析,得到不同的功能类。在此基础上提出了从功能类中抽取出不同模型元素的方法,构造初始模型。·针对形式化规约的获取问题,本文提出了一种基于领域知识的自然语言到LTL规约的自动生成方法。该方法首先对自然语言规约进行解析,然后从语法树中识别关键节点,抽取出相应的语义信息和时序逻辑信息,生成树形中间表示形式。最后利用模板将所有子句转换成原子命题,并提出一种基于深度优先搜索的算法,将原子命题与时序操作符、逻辑操作符结合,由树结构生成LTL规约。针对自然语言的结构歧义问题,本文提出了一种基于领域知识的结构歧义消除方法,能够自动检测并修正语法树中的结构歧义。·本文实现了设备辅助建模工具和LTL规约生成工具。为了验证工具在真实数据集上的执行效果,本文实施了一项调研工作,收集用户给出的规则和自然语言规约。本文在IFTTT功能描述集和自然语言规约数据集上展开评估实验,并将生成的模型和LTL规约用于验证真实用户构建的智能场景。实验结果显示,我们的工具在正确率和效率上都有很好的表现,而且生成的模型和LTL规约能够有效地帮助用户发现智能家居场景中的错误。

关键词：事件驱动物联网智能家居模型抽取线性时序逻辑自然语言处理

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

电力二次设备配线工艺数字化研究

智能制造 2022年第3期 68-72页

作者：王广彬曹齐崔永艳林峰俞俊国电南瑞科技股份有限公司江苏南京211106 南瑞集团有限公司(国网电力科学研究院) 江苏南京211106

目前电力二次设备配线工艺多样化、工序分散、作业效率低,线长预估不准导致浪费,而使用三维工艺设计软件要求产品标准化程度高,与生产自动化设备衔接不足,配线工艺设计已成为制约电力二次设备生产加工的瓶颈问题。本文给出了一种基于数... 详细信息

目前电力二次设备配线工艺多样化、工序分散、作业效率低,线长预估不准导致浪费,而使用三维工艺设计软件要求产品标准化程度高,与生产自动化设备衔接不足,配线工艺设计已成为制约电力二次设备生产加工的瓶颈问题。本文给出了一种基于数字化的电力二次设备配线工艺设计方法,通过对配线工艺电气器件的数字化模型抽取、配线布局规则的参数化设置,实现了从电气设计到生产制造环节的数字语言统一、数据流连续可用。该方法已在新一代智能变电站示范工程中得到应用,达到了提升工艺设计效率、整合作业工序、节约人工成本的目的。

关键词：数字化配线工艺模型抽取参数化作业工序