刘剑

作品数：9被引量：19H指数：3
导出分析报告
供职机构：中国科学院软件研究所更多>>
发文主题：初始化ANDROID漏洞分析系统代码传值进程更多>>
发文领域：自动化与计算机技术文化科学更多>>
发文期刊：《清华大学学报（自然科学版）》《计算机系统应用》《计算机应用与软件》《载人航天》更多>>
所获基金：国家自然科学基金中国科学院知识创新工程重要方向项目载人航天领域预先研究项中国科学院知识创新工程更多>>
-
在结果中检索

检索结果分析

署名顺序

  • 全部
  • 第一作者
结果分析中...
共 条 记 录，以下是1-9
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
一种基于微内核操作系统进程间通信恢复方法
《计算机应用与软件》2015年第6期9-13,共5页孙可钦 王玉庆 刘剑 杨秋松 马越 
国家自然科学基金项目(61305054);中国科学院知识创新工程重要方向性项目(KGCX2-YW-12);国家"核高基"重大科技专项(2010ZX01036-001-002-2)
微内核架构为操作系统提供了良好的隔离性,高度模块化的架构设计使得微内核架构操作系统对进程间通信的依赖度极高,进程间通信恢复是系统恢复正常运行的关键。权能是微内核架构操作系统中进程对资源操作权限的描述,决定进程间能否进行...
关键词：微内核 操作系统安全 进程间通信 可信恢复 
一种基于单条程序执行路径的错误定位方法
《计算机系统应用》2014年第10期112-118,共7页周艺 易秋萍 刘剑 淮晓永 
中国科学院知识创新工程重要方向性项目(KGCX2-YW-12);国家"核高基"重大科技专项(2010ZX01036-001-002-2);国家自然科学基金青年基金(61305054)
当程序在测试中发生错误时,将形成一条错误的程序执行路径,程序员将会花费很多精力去检测程序代码和定位最终的程序错误.提出一种基于单条程序执行路径的错误定位方法,该方法通过对程序进行反向执行,计算出多个最弱前置条件及其相对应...
关键词：错误定位 最弱前置条件 可满足性理论 动态分析 自动化测试 
基于锁信息的多线程软件原子性错误检测方法被引量：1
《计算机应用与软件》2014年第6期1-4,94,共5页王云飞 刘剑 马越 
核高基项目(2012ZX01039-004);中国科学院知识创新工程项目(KGCX2-YW-125)
原子性错误是多线程软件开发中常见的并发错误之一。传统的静态分析方法存在误报的可能,动态方法由于利用的信息过少而存在运行效率低下的问题。针对以上问题,设计以动态方法为基础通过计算锁信息,根据锁信息判断是否可能发生原子性错...
关键词：多线程软件 原子性错误 锁信息 模型检测 动态优化 
航天嵌入式操作系统的分析与验证被引量：3
《载人航天》2012年第6期69-74,共6页李斌 马越 李潇 刘剑 
载人航天领域预先研究项目(000301);国家自然科学基金项目(61003028;61073044;60903051)
在介绍航天嵌入式操作系统的特点和应用概况的基础上,阐述了对航天嵌入式操作系统进行自动分析与验证的必要性,综述了自动分析和验证技术,并重点介绍了模型检测和符号执行两种分析技术,列举了领域内近年来具有代表性的工具及分析实例。...
关键词：嵌入式操作系统 分析验证 静态分析 模型检测 符号执行 航天系统 
一种并发程序原子性错误的检测方法及工具被引量：2
《计算机应用与软件》2012年第11期92-94,100,共4页李潇 刘剑 易秋萍 
国家"核高基"重大科技专项(2010ZX01036-001-002-2);中国科学院知识创新工程重要方向性项目(KGCX2-YW-12)
原子性错误的检测对于多线程程序并发错误的分析有着重要意义,其检测难点在于从违反原子性的情况中识别出会导致程序出错的执行序列。为了解决这个问题,采用测试训练提取原子性迁移对集合以及模型检测方法,提出原子性错误自动检测算法MC...
关键词：多线程程序 原子性错误 线程序列的不确定 模型检测 
基于控制流挖掘的Android系统代码漏洞分析被引量：7
《清华大学学报（自然科学版）》2012年第10期1335-1339,共5页刘剑 孙可钦 汪孙律 
中国科学院知识创新工程重要方向资助项目(KGCX2-YW-125);国家重点科技专项“核高基”资助项目(2010ZX01036-001-002,2010ZX01037-001-002)
Android操作系统被广泛应用于智能手机、平板电脑等便携移动设备,因此Android操作系统的安全性和可靠性至关重要。本文使用控制流挖掘方法,针对Android内核代码的多种典型错误构建相关的分析脚本,进行了分析检测,并对Android系统多版本...
关键词：控制流挖掘 漏洞分析 ANDROID操作系统 
面向访问验证保护级的安全VMM形式化原型系统设计和实现
《计算机科学》2010年第12期85-90,共6页易秋萍 刘剑 武术 
中国科学院知识创新工程重要方向项目“面向访问验证保护级的安全操作系统原型系统研发(KGCX2-YW-125)”;北京市科技创新项目“安全可信操作系统研制(Z08000102000801)”;计算机科学国家重点实验室开放课题“面向高等级安全操作系统的形式化保证技术研究(SYSKF0909)”资助
操作系统是计算机软件系统的基础,具有控制逻辑复杂、安全性和可靠性要求高等特点。在国内外高等级安全操作系统的规范和标准中,都提出了对内核进行形式化规范和验证的要求。近年来国内相关研究机构相继开发了满足GB 17859-1999"强制访...
关键词：安全操作系统 VMM HASKELL MONAD 形式化原型 
谓词μ演算和模态图的语义一致性被引量：3
《软件学报》2003年第10期1672-1680,共9页刘剑 林惠民 
国家自然科学基金~~
模态图是谓词m演算的一种有效的图形表示形式.证明了谓词m演算和模态图的语义一致性,详细讨论了谓词m演算公式、嵌套谓词等式系和模态图之间的关系,并给出了一种优化的从线性公式到嵌套谓词等式系的转换算法.
关键词：不动点 谓词μ演算 嵌套谓词等式系 模态图 
传值进程模型检测中诊断信息的生成被引量：3
《软件学报》2003年第1期1-8,共8页刘剑 林惠民 
(国家自然科学基金)No.69833020 ~
诊断信息自动生成是模型检测方法的基本特征之一,对分析和排错具有重要的意义.讨论了传值进程模型检测中诊断信息的生成问题.引入了两种诊断信息的表示结构:证明图和示例;提出了两种诊断信息构造算法.所采用的方法是从检测过程保存的依...
关键词：传值进程 模型检测 诊断信息 进程代数 证明图 示例 算法 计算机 
全选清除导出
共1页<1>
检索报告 对象比较 聚类工具 使用帮助 返回顶部