检索结果-南通市图书馆

多线程Java程序安全行为模型的静态检查方法

在线全文

学校读者我要写书评

暂无评论

计算机学报 2009年第9期32卷 1856-1868页

作者：金英李泽鹏张晶刘磊吉林大学计算机科学与技术学院长春130012

多线程作为支持程序结构化和并行化的重要机制,其应用越来越广泛,多线程应用程序的安全性也成为新的研究热点之一.针对Java多线程程序,文中采用参数化扩展上下文无关文法作为其安全相关行为模型的抽象表示,给出了从多线程Java程序自动... 详细信息

多线程作为支持程序结构化和并行化的重要机制,其应用越来越广泛,多线程应用程序的安全性也成为新的研究热点之一.针对Java多线程程序,文中采用参数化扩展上下文无关文法作为其安全相关行为模型的抽象表示,给出了从多线程Java程序自动生成安全相关行为模型的方法,形式地描述了静态检查该模型是否满足安全策略的实现,并应用到携带模型代码方法的实现框架中.该方法为安全执行非信任多线程Java移动代码提供了有效支持.

关键词：多线程Java程序安全相关行为模型静态检查参数化扩展上下文无关文法

在线全文

学校读者我要写书评

暂无评论

基于开源JVM的安全策略强制实施

电子学报 2009年第B04期37卷 36-41页

作者：魏达金英张晶郑晓娟李卓吉林大学计算机科学与技术学院吉林长春130012 东北师范大学软件学院吉林长春130117

非信任代码的安全执行是移动代码安全的重要问题之一.携带模型代码(Model Carrying Code)方法同时考虑了移动代码生产者和使用者对安全性的支持和需求,建立了以模型为中心的安全执行非信任代码的理论框架,其中安全策略的定义和强制实施... 详细信息

非信任代码的安全执行是移动代码安全的重要问题之一.携带模型代码(Model Carrying Code)方法同时考虑了移动代码生产者和使用者对安全性的支持和需求,建立了以模型为中心的安全执行非信任代码的理论框架,其中安全策略的定义和强制实施是MCC方法的重要组成部分之一.本文针对已被广泛使用的Java移动代码,以开源JVM Kaffe和Linux操作系统为研究载体,提出了基于开源JVM的安全策略实施模型,并实现从安全策略定义到实施的整个过程.本文在安全策略规范描述,可强制实施的扩展有限自动机(EFSA)模型和进程级监视以捕获系统调用等方面都做了有益的尝试,为完善MCC方法和实现安全策略的强制实施提供很好的方案.

关键词：携带模型代码安全策略描述和实施开源JVM 进程级监视

在线全文

学校读者我要写书评

暂无评论

基于压缩编码的经典最优规划方法

吉林大学学报（工学版） 2010年第6期40卷 1644-1649页

作者：吕帅刘磊江鸿魏唯吉林大学计算机科学与技术学院长春130012

在基于Graphplan的编码方式的基础上,设计了基于PMA的编码方式,并从理论上证明了该编码方式的有效性;提出了编码求解过程中的一种目标状态预处理策略;设计并实现了相应的规划系统PMA-SP,并利用国际规划竞赛选用的Benchmark问题予以测试... 详细信息

在基于Graphplan的编码方式的基础上,设计了基于PMA的编码方式,并从理论上证明了该编码方式的有效性;提出了编码求解过程中的一种目标状态预处理策略;设计并实现了相应的规划系统PMA-SP,并利用国际规划竞赛选用的Benchmark问题予以测试。结果表明:与SATPLAN2006相比,对于顺序规划域Blocks World,编码规模压缩了40%,求解效率提高了2倍;对于并发规划域Logistics,编码规模压缩了80%以上,求解效率各有好坏,PMA-SP对于所测两类规划域编码规模有所压缩,求解效率也有一定程度的提高。

关键词：人工智能基于可满足性的规划基于Graphplan的编码互斥公理规划系统

基于多语言范例的“形式语义学”教学辅助系统

在线全文

学校读者我要写书评

暂无评论

吉林大学学报(理学版) 2009年第3期47卷 530-536页

作者：金英郑晓娟张晶孙旭东吉林大学计算机科学与技术学院东北师范大学软件学院

针对简单函数式语言、简单过程式语言和简单面向对象式语言等多个程序语言范例,分别定义了它们的操作语义和指称语义,同时设计了一个"形式语义学"教学辅助系统,用于演示不同语言范例程序的基于形式语义定义的可视化解释,该系统使学生可... 详细信息

针对简单函数式语言、简单过程式语言和简单面向对象式语言等多个程序语言范例,分别定义了它们的操作语义和指称语义,同时设计了一个"形式语义学"教学辅助系统,用于演示不同语言范例程序的基于形式语义定义的可视化解释,该系统使学生可以通过形象生动的动态演示和同步解释,充分理解和掌握程序设计语言的形式语义及其实现.

关键词：形式语义学可视化教学辅助系统增量式设计实践驱动教学

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

Pi演算与动态描述逻辑DDL的关系研究

计算机研究与发展 2008年第z1期45卷 131-136页

作者：刘磊汪美玲高艳华张长海于哲舟吉林大学计算机科学与技术学院长春130012

分析了Pi演算与动态描述逻辑DDL之间的关系:DDL分别从静态结构与动态结构两方面对Pi演算的若干过程定义进行描述,体现了过程的逻辑结构及过程间逻辑关系的变化;以一种基于Pi演算的过程模型为基础,分析了ALC描述逻辑、TBox和ABox的语义,... 详细信息

分析了Pi演算与动态描述逻辑DDL之间的关系:DDL分别从静态结构与动态结构两方面对Pi演算的若干过程定义进行描述,体现了过程的逻辑结构及过程间逻辑关系的变化;以一种基于Pi演算的过程模型为基础,分析了ALC描述逻辑、TBox和ABox的语义,并通过一个例子说明Pi演算对DDL动态知识的变化过程的描述.以上工作表明:DDL的可判定推理可解决基于Pi演算的动态系统的某些一致性检测问题,而Pi演算对动态系统的描述能力可解决DDL动态知识的变化过程的描述问题.

关键词： Pi演算动态描述逻辑DDL 关系

在线全文

学校读者我要写书评

暂无评论

基于自动推理技术的智能规划方法

软件学报 2009年第5期20卷 1226-1240页

作者：吕帅刘磊石莲李莹吉林大学计算机科学与技术学院吉林长春130012 吉林大学符号计算与知识工程教育部重点实验室吉林长春130012

对几种智能规划方法中利用的逻辑演绎与推理技术予以分析,分别介绍利用命题逻辑的基于可满足性的规划方法与规划系统,利用模态逻辑与析取推理的Conformant规划方法与规划系统,利用非单调逻辑的规划方法和利用模糊描述逻辑的Flexible规... 详细信息

对几种智能规划方法中利用的逻辑演绎与推理技术予以分析,分别介绍利用命题逻辑的基于可满足性的规划方法与规划系统,利用模态逻辑与析取推理的Conformant规划方法与规划系统,利用非单调逻辑的规划方法和利用模糊描述逻辑的Flexible规划方法,并结合国际规划竞赛和相关论文等的实验结论说明上述方法的有效性和可行性.最后,提出目前基于自动推理技术的智能规划方法所面临的挑战、可能的处理方法以及与之相关的研究热点与趋势.

关键词：智能规划命题逻辑模态逻辑非单调逻辑描述逻辑自动推理可满足性

在线全文

学校读者我要写书评

暂无评论

基于Java平台实现安全行为模型验证

计算机工程与科学 2007年第10期29卷 7-10页

作者：李泽鹏金英张晶郑晓娟吉林大学计算机科学与技术学院吉林长春130012 东北师范大学软件学院吉林长春130117

非信任代码的安全执行是移动代码安全的重要问题之一。携带模型代码方法同时从移动代码的生产者和使用者的角度考虑,为安全执行非信任代码提供了一个系统、全面且有效的解决方案。该方法主要包括安全策略的定义、安全行为模型的生成,以... 详细信息

非信任代码的安全执行是移动代码安全的重要问题之一。携带模型代码方法同时从移动代码的生产者和使用者的角度考虑,为安全执行非信任代码提供了一个系统、全面且有效的解决方案。该方法主要包括安全策略的定义、安全行为模型的生成,以及其验证和安全策略的强制实施。针对已被广泛使用的Java平台,在深入分析其基于访问控制的安全体系结构的基础上,通过对Java核心类的修改和扩展,提出了一种能增加新的安全策略,以及实现MCC方法中安全行为模型验证的方法,为提高Java安全策略的描述能力,以及基于Java平台实现MCC方法,确保更全面的安全机制提供了可行的途径。

关键词：携带模型代码 Java安全机制安全行为模型形式验证

在线全文

学校读者我要写书评

暂无评论

基于小波变换的全局能量图像融合算法

吉林大学学报（工学版） 2009年第S1期39卷 232-236页

作者：刘磊张红王莎吉林大学计算机科学与技术学院长春130012 吉林大学集成光电子学国家重点联合实验室吉林大学实验区电子科学与工程学院长春130012

提出了一种基于小波变换的全局能量图像融合算法。对小波分解系数采用基于全局匹配度来选择和加权的融合规则。全局匹配度以区域能量作为测度,包含了小波分解的高频3个方向的匹配度。使得选择策略下融合图像的高频3个方向的小波系数均... 详细信息

提出了一种基于小波变换的全局能量图像融合算法。对小波分解系数采用基于全局匹配度来选择和加权的融合规则。全局匹配度以区域能量作为测度,包含了小波分解的高频3个方向的匹配度。使得选择策略下融合图像的高频3个方向的小波系数均来自同一源图像,保证了小波重构时融合的一致性。实验结果表明,全局能量法的融合图像具有更好的融合特性。

关键词：图像融合小波分解匹配度区域能量

在线全文

学校读者我要写书评

暂无评论

基于量化布尔公式的条件规划编码方式

计算机科学 2010年第11期37卷 252-256,281页

作者：高冰冰张长海吕帅吉林大学计算机科学与技术学院长春130012

介绍条件规划问题及其相关的求解系统,着重分析以逻辑为基础的编码方式。针对基于量化布尔公式的转换方法进行详细分析,给出3种不同形式的量化布尔公式编码。最后,对这3种编码进行比较,分析基于命题逻辑公式与量化布尔公式这两种不同转... 详细信息

介绍条件规划问题及其相关的求解系统,着重分析以逻辑为基础的编码方式。针对基于量化布尔公式的转换方法进行详细分析,给出3种不同形式的量化布尔公式编码。最后,对这3种编码进行比较,分析基于命题逻辑公式与量化布尔公式这两种不同转换方式的优劣,讨论基于量化布尔公式的规划方法未来的研究方向和发展趋势。

关键词：条件规划不确定性规划量化布尔公式编码