检索结果-南通市图书馆

在线全文

学校读者我要写书评

暂无评论

命题投影时序逻辑并发建模与自动验证

华中科技大学学报（自然科学版） 2010年第8期38卷 77-80页

作者：朱维军张海宾周清雷西安电子科技大学计算机学院陕西西安710071 郑州大学信息工程学院河南郑州450052

针对目前尚无模型检测方法对区间并发模型进行区间性质的自动验证的情况,采用命题投影时序逻辑中具有特定结构的一类公式来建立系统的区间并发模型,该逻辑的任意公式可以描述模型需要满足的区间性质,通过归约为已有的逻辑公式可满足性... 详细信息

针对目前尚无模型检测方法对区间并发模型进行区间性质的自动验证的情况,采用命题投影时序逻辑中具有特定结构的一类公式来建立系统的区间并发模型,该逻辑的任意公式可以描述模型需要满足的区间性质,通过归约为已有的逻辑公式可满足性判定算法,证明了命题投影时序逻辑统一框架模型检测是可判定的,从而得到了其自动验证方法,并给出了一个验证实例.

关键词：模型检测时序逻辑可计算性与判定性命题投影时序逻辑并发模型统一逻辑框架

在线全文

学校读者我要写书评

暂无评论

C语言程序设计案例精粹 4

2010年

作者：朱维军

本书内容包括C语言开发环境、数据类型、运算符、控制语句、输入与输出、数组、函数、指针、结构体与共用体、链表、编译预处理、文件、字符串处理、调试、软件测试、常用算法, 以及C语言的实际应用和工程应用等。

ISBN: (纸本)9787894646859

关键词： C语言

来源：畅想之星图书光盘版（南... 评论

在线全文

畅想之星图书光盘版（南通市图书馆镜像）

学校读者我要写书评

暂无评论

我国果蔬产业发展存在的问题及对策

河南农业科学 2002年第2期31卷 26-27页

作者：朱维军河南省农业学校中牟451450

随着我国农村经济结构调整,果蔬种植面积和总产量都有大幅度的提高.2000年我国果品总产量达600亿kg,人均近50 kg;蔬菜总产量达4 400亿 kg,人均350 kg.果蔬产品的逐渐丰富,基本满足了城乡居民的生活需要,实现了周年供应;但由于贮藏加工... 详细信息

随着我国农村经济结构调整,果蔬种植面积和总产量都有大幅度的提高.2000年我国果品总产量达600亿kg,人均近50 kg;蔬菜总产量达4 400亿 kg,人均350 kg.果蔬产品的逐渐丰富,基本满足了城乡居民的生活需要,实现了周年供应;但由于贮藏加工业发展缓慢,特别是采后处理技术严重落后,造成果蔬腐烂,损耗率较高,市场竞争能力较低,影响农村经济的发展.因此提高果蔬产品的质量,发展贮藏加工业,是我国果蔬产业发展亟待解决的问题.

关键词：中国果蔬产业问题发展基地建设商品化处理贮藏加工业产业化

在线全文

学校读者我要写书评

暂无评论

多组分非理想物系精馏研究

多组分非理想物系精馏研究

作者：朱维军华侨大学

学位级别：硕士

本文进行多组分非理想物系精馏传质过程的理论和试验研究。化工生产中分离的物系绝大部分是多组分非理想物系，最常用、最重要的化工单元操作是精馏，因此，开展多组分非理想物系精馏传质过程研究具有理论和应用两方面的重要意义。本... 详细信息

本文进行多组分非理想物系精馏传质过程的理论和试验研究。化工生产中分离的物系绝大部分是多组分非理想物系，最常用、最重要的化工单元操作是精馏，因此，开展多组分非理想物系精馏传质过程研究具有理论和应用两方面的重要意义。本文的研究工作主要分为三部分。第一部分工作是开展多组分物系传质过程的理论研究。多组分物系传质过程与二组分物系传质过程有着本质的区别，前者远比后者复杂。多组分传质过程各组分的点效率不相等，某些组分的点效率可能小于零、大于1或趋于无穷大。描述多组分物系传质过程的基本方程是Maxwell-Stefan(MS)方程和普遍化Fick定律，由这些方程发展的多组分物系传质过程的理论，可以合理地阐释发生于多组分物系的传质奇异现象。本文的第二部分工作是开展多组分非理想物系精馏传质过程的模拟研究。有关精馏过程模拟的研究工作已经开展了很多，但是大部分模拟采用平衡级模型，研究的物系大部分是简单的二组分物系。对于操作中两相的具体情况与平衡状态之间的差异，常用的处理方法是引入效率因子。而在实际操作过程中，当处理体系为两组分以上物系，尤其当物系具有一定的非理想性时，体系中各组分的效率值并不相同，有时差别很大，因此，平衡级模型模拟与实际情况之间存在较大偏差。本文在多组分传质过程理论的基础上建立了一个非平衡级精馏模拟模型，该模型考虑多组分物系中组分间的交互作用，具有广泛的适用性。本文先建立一个通用的分离级的物理模型，结合物料衡算、能量衡算、传递速率计算、界面相平衡计算，结合多组分传质过程计算，建立一个通用的数学模型，再将通用模型应用于精馏过程。通过严格算法，对所建立的多组分精馏过程数学模型进行求解。结果显示，非平衡级模型比平衡级模型能够更准确地对精馏过程进行模拟。本文第三部分的工作是开展多组分非理想物系精馏传质过程试验研究。研究表明，本文在多组分传质过程理论的基础上建立的非平衡级精馏模拟模型与试验结果较吻合。

关键词：多组分精馏模拟平衡级非平衡级多组分传质

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

以DNA为载体的线性时序逻辑模型检测

电子学报 2016年第6期44卷 1265-1271页

作者：朱维军周清雷李永亮郑州大学信息工程学院河南郑州450001

线性时序逻辑模型检测被广泛应用于处理器设计与验证、网络协议验证、安全协议验证等领域.然而到目前为止,该技术只能在电子计算的平台上实现.为了以脱氧核糖核酸(Deoxyribo Nucleic Acid,DNA)为载体对线性时序逻辑(Linear Temporal Log... 详细信息

线性时序逻辑模型检测被广泛应用于处理器设计与验证、网络协议验证、安全协议验证等领域.然而到目前为止,该技术只能在电子计算的平台上实现.为了以脱氧核糖核酸(Deoxyribo Nucleic Acid,DNA)为载体对线性时序逻辑(Linear Temporal Logic,LTL)实施模型检测,给出了使用粘贴自动机实现Until算子模型检测的方法.首先,使用粘贴自动机对Until公式的有穷状态自动机(Finite State Automata,FSA)模型进行编码;然后,将系统模型转换为粘贴自动机的输入字符串;最后,用粘贴自动机验证系统是否满足公式.仿真实验结果证实,新方法可实现对LTL逻辑时序算子的检测.

关键词：模型检测脱氧核糖核酸线性时序逻辑粘贴自动机

在线全文

学校读者我要写书评

暂无评论

离散时间区间时序逻辑可满足性的判定

电子学报 2010年第5期38卷 1039-1045页

作者：朱维军张海宾周清雷西安电子科技大学计算机学院陕西西安710071 郑州大学信息工程学院河南郑州450052

目前还没有模型检查的方法自动检测模型是否满足时间区间时序逻辑描述的性质.我们约束时间域到离散时间,证明了离散时间区间时序逻辑的可满足性是可判定的,因而是可模型检查的.提出了时间正则图模型,通过从离散时间区间时序逻辑到时间... 详细信息

目前还没有模型检查的方法自动检测模型是否满足时间区间时序逻辑描述的性质.我们约束时间域到离散时间,证明了离散时间区间时序逻辑的可满足性是可判定的,因而是可模型检查的.提出了时间正则图模型,通过从离散时间区间时序逻辑到时间正则图的构造,提出了基于该逻辑的判定算法,该算法可以推广到其它的时序逻辑模型检查,并优于现有的基于自动机的时序逻辑判定方法.

关键词：模型检查离散时间区间时序逻辑时间正则图可满足性判定

Intrusion Detection Algorithm Based on Model Checking Interval Temporal Logic

在线全文

学校读者我要写书评

暂无评论

China Communications 2011年第3期8卷 66-72页

作者：朱维军王忠勇张海宾 School of Computer Science Xidian University School of Information Engineering Zhengzhou University

Model checking based on linear temporal logic reduces the false negative rate of misuse ***,linear temporal logic formulae cannot be used to describe concurrent attacks and piecewise *** there is still a high rate of false negatives in detecting these complex attack *** solve this problem,we use interval temporal logic formulae to describe concurrent attacks and piecewise *** this basis,we formalize a novel algorithm for intrusion detection based on model checking interval temporal *** with the method based on model checking linear temporal logic,the new algorithm can find unknown succinct *** simulation results show that the new method can effectively reduce the false negative rate of concurrent attacks and piecewise attacks.

关键词： network security intrusion detection misuse detection interval temporal logic model checking

在线全文

学校读者我要写书评

暂无评论

基于DNA计算的线性时序逻辑模型检测方法

计算机学报 2016年第12期39卷 2578-2597页

作者：朱维军周清雷张钦宪郑州大学信息工程学院郑州450001 郑州大学基础医学院郑州450001

该文研究基于脱氧核糖核酸(Deoxyribonucleic Acid,DNA)计算的线性时序逻辑(Linear Temporal Logic,LTL)模型检测问题.为此,该文给出了使用粘贴自动机实现LTL模型检测的方法.首先,使用3′-5′型单链DNA分子对LTL公式的有穷状态自动机(Fi... 详细信息

该文研究基于脱氧核糖核酸(Deoxyribonucleic Acid,DNA)计算的线性时序逻辑(Linear Temporal Logic,LTL)模型检测问题.为此,该文给出了使用粘贴自动机实现LTL模型检测的方法.首先,使用3′-5′型单链DNA分子对LTL公式的有穷状态自动机(Finite State Automata,FSA)模型进行编码,从而获得实现公式的粘贴自动机;其次,使用5′-3′型单链DNA分子对系统模型进行编码,从而获得粘贴自动机的输入字符串;最后,对表征粘贴自动机的DNA单链分子和表征输入字符串的DNA单链分子实施一系列生化反应,即可判定系统是否满足公式.分子生物学仿真实验结果表明:给出的DNA编码序列能达到99.9%的碱基配对正确率,且新方法成功地对所有4种LTL基本公式与5种LTL常见公式实施了检测;与之对照,已有的方法只能有效检测1种LTL基本公式与0种LTL常见公式.在此基础上,对本实验给出的DNA编码方案直接作位数扩展即可拥有对任意给定LTL一般公式的(理论)检测能力.

关键词：模型检测脱氧核糖核酸线性时序逻辑粘贴自动机有穷状态自动机 DNA计算

在线全文

学校读者我要写书评

暂无评论

基于时间自动机若干新模型的研究

基于时间自动机若干新模型的研究

作者：朱维军郑州大学

学位级别：硕士

时间自动机被广泛用于实时系统验证和模型检测。一方面出现了很多算法和工具;另一方面有不少基于时间自动机的不同模型被提出,以适应不同类型的系统验证。信号自动机与时间树自动机是两个新提出的模型。时间树自动机理论还很不完善,目... 详细信息

时间自动机被广泛用于实时系统验证和模型检测。一方面出现了很多算法和工具;另一方面有不少基于时间自动机的不同模型被提出,以适应不同类型的系统验证。信号自动机与时间树自动机是两个新提出的模型。时间树自动机理论还很不完善,目前主要是基于时间树自动机识别的语言类及相关性质的研究。本文提出了一个时间树自动机识别语言的一个条件,并证明了结论的正确性。如果一个语言不能满足该条件,它一定不能被时间树自动机识别。这为证明一个具体语言不能被时间树自动机识别提供了思路。信号自动机为一类实时系统建立了比普通时间自动机更适合的模型。本文通过对信号自动机与时间自动机的模型对比与深入分析,证明了两种模型的行为等价关系,并提出了互模拟算法,这样信号自动机验证问题被归约为时间自动机验证问题。如果把这样的互模拟算法与时间自动机验证算法组合在一起,就可以得到信号自动机验证算法,以便在此基础上开发出信号自动机验证工具。在基因工程中,形式化方法被用于预测人工基因网络控制生物基因网络的行为结果,这种预测已经在生物医药研制与开发领域发挥了很大作用。目前已有的基于有限状态自动机的方法的局限是不能描述系统时间约束。本文提出了基于时间自动机的基因网络逻辑模型,以计算时间约束下控制基因网络的行为。

关键词：时间自动机时间树自动机信号自动机基因网络离散步长双向模拟识别语言