江苏省“六大人才高峰”高层次人才项目(2011-DZXX-035)

作品数：11被引量：46H指数：4
导出分析报告
相关作者：钱振江黄皓宋方敏刘苇李康杰更多>>
相关机构：南京大学常熟理工学院伦敦大学更多>>
相关期刊：《计算机学报》《软件导刊》《电子学报》《计算机应用与软件》更多>>
相关主题：形式化设计形式化验证操作系统定理证明ISABELLE更多>>
相关领域：自动化与计算机技术医药卫生理学更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
微内核架构内存管理的形式化设计和验证方法研究被引量：4
《电子学报》2017年第1期251-256,共6页钱振江 刘永俊 姚宇峰 汤力 黄皓 宋方敏 
国家自然科学基金(No.61402057);江苏省科技计划自然科学研究项目(No.BK20140418);中国博士后科学基金(No.2015M571737);江苏省"六大人才高峰"高层次人才项目(No.2011-DZXX-035);江苏省高校自然科学研究项目(No.12KJB520001)
由于巨大的规模和复杂性,操作系统的设计和实现的正确性很难用传统的定量方法来描述.本文阐述对微内核操作系统的形式化设计和验证的方法.在汇编层利用非确定性自动机对系统进行形式化建模,并使用Hoare三元组描述模块接口函数的前后置条...
关键词：操作系统 内存管理 形式化设计 形式化验证 定理证明 
操作系统汇编级形式化设计和验证方法被引量：3
《软件学报》2016年第12期3143-3157,共15页钱振江 黄皓 宋方敏 
国家自然科学基金(61402057);江苏省科技计划自然科学研究项目(BK20140418);中国博士后科学基金(2015M571737);江苏省“六大人才高峰”高层次人才项目(2011-DZXX-035);江苏省高校自然科学研究项目(12KJB520001)~~
由于系统的巨大规模,操作系统设计和实现的正确性很难用传统的方法进行描述和验证.在汇编层形式化地对系统模块的功能语义进行建模,提出一种汇编级的系统状态模型,作为汇编语言层设计和验证的纽带.通过定义系统状态模型的合法状态和状...
关键词：操作系统 正确性验证 形式化方法 系统状态模型 
一种Android系统上对应用程序权限进行限制的方法
《计算机应用与软件》2014年第6期308-311,333,共5页鲁亚峰 宁强 钱振江 黄皓 
国家高技术研究发展计划项目(2011AA01A202);国家自然科学基金项目(61021062);江苏省"六大人才高峰"高层次人才项目(2011-DZXX-035);江苏省高校自然科学研究项目(12KJB520001)
Android系统上的安装系统存在着"全部同意或取消安装"的问题,即用户同意应用程序要求的所有权限或取消安装,这使用户不能够灵活地限制应用程序的权限。通过修改Android系统上的安装系统和包权限检查系统,可以实现对应用程序权限的动态...
关键词：ANDROID系统 安装系统 应用程序权限 动态约束 
操作系统形式化设计与安全需求的一致性验证研究被引量：6
《计算机学报》2014年第5期1082-1099,共18页钱振江 黄皓 宋方敏 
国家自然科学基金创新研究群体基金(60721002);江苏省"六大人才高峰"高层次人才项目(2011-DZXX-035);江苏省高校自然科学研究项目(12KJB520001);CSLG科研项目(QT1312)资助~~
采用数学形式化方法对操作系统进行设计和验证可以保证系统的高度安全性.目前已有的操作系统形式化研究工作主要是验证系统的实现在代码级的程序正确性.提出一种操作系统形式化设计和验证的方法,采用操作系统对象语义模型(OSOSM)对系统...
关键词：操作系统 形式化设计 安全需求 一致性验证 定理证明 信息安全 网络安全 
微内核架构文件系统的形式化设计与验证方法研究被引量：4
《小型微型计算机系统》2013年第10期2261-2266,共6页钱振江 唐洪英 李康杰 黄皓 宋方敏 
国家"八六三"高技术研究发展计划项目(2011AA01A202)资助;国家自然科学基金创新研究群体基金项目(60721002)资助;江苏省"六大人才高峰"高层次人才项目(2011-DZXX-035)资助;江苏省高校自然科学基金项目(12KJB520001)资助
文件系统作为数据存储和管理的功能模块,其正确性是操作系统安全性的重要方面.采用形式化方法对微内核架构文件系统进行设计,使用操作系统对象语义模型(OSOSM)框架提出微内核架构文件系统的状态自动机模型,并依此描述系统调用的功能语...
关键词：文件系统 微内核架构 形式化设计 形式化验证 正确性断言 ISABELLE HOL 
微内核架构多线程机制的形式化设计研究被引量：5
《计算机科学》2013年第4期136-141,163,共7页钱振江 卢亮 黄皓 
国家高技术研究发展计划(863)(2011AA01A202);江苏省"六大人才高峰"高层次人才项目(2011-DZXX-035);江苏省高校自然科学研究项目(12KJB520001)资助
微内核架构因其有效的模块隔离性而成为操作系统方面研究的热点,多线程机制是微内核架构需要解决的关键性能问题。有不少的工作对微内核架构多线程机制进行了研究,但存在频繁的系统地址空间切换和实现复杂度高的问题。采用形式化的方式...
关键词：微内核 多线程 操作系统 形式化描述 形式化设计 
微内核中断机制的形式化设计与验证被引量：4
《计算机科学》2013年第3期197-200,205,共5页李康杰 钱振江 黄皓 
国家高技术研究发展计划(863)(2011AA01A202);江苏省"六大人才高峰"高层次人才项目(2011-DZXX-035);江苏省高校自然科学研究项目(12KJB520001)资助
操作系统的正确性和安全性很难用定量的方法进行描述。形式化方法是操作系统设计和验证领域公认的标准方法。以操作系统对象语义模型(OSOSM)为基础,采用形式化方法对微内核架构的中断机制进行了设计和验证,在自行开发的安全可信操作系统...
关键词：形式化设计 形式化验证 微内核 中断 完整性 
操作系统对象语义模型(OSOSM)及形式化验证被引量：11
《计算机研究与发展》2012年第12期2702-2712,共11页钱振江 刘苇 黄皓 
国家"八六三"高技术研究发展计划基金项目(2011AA01A202);江苏省科技支撑计划基金项目(BE2008124);国家自然科学基金创新研究群体项目(60721002);江苏省"六大人才高峰"高层次人才项目(2011-DZXX-035);江苏省高校自然科学研究项目(12KJB520001)
操作系统的复杂性使得其安全性问题日益突出.有不少的研究工作采用形式化的方式对现有的操作系统进行了正确性的验证,这些工作主要是采用程序形式逻辑验证代码级的功能实现性.从系统设计的角度,以高阶逻辑和类型论为基础,提出了操作系...
关键词：操作系统对象 语义模型 形式化设计 安全性验证 Isabelle定理证明 
VTOS:一个支持多核的微内核操作系统设计与实现
《软件导刊》2012年第10期125-129,共5页景香博 陈江 钱振江 
863计划重大项目(2011AA01A202);国家自然科学基金项目(61021062);江苏省"六大人才高峰"高层次人才项目(2011-DZXX-035)
现在处理器的发展已经进入了一个新的时代,继承了几十乃至上百个核心的处理器已经出现。这在大大提升了硬件处理能力的同时,也给软件设计,尤其是操作系统设计带来了很大困难。为了提高系统的可扩展性,操作系统开发人员需要花费大量的精...
关键词：多核 微内核 操作系统 可扩展性 同步 
基于Poincare差值散点图的心率变异性分析方法研究被引量：14
《物理学报》2012年第19期62-69,共8页霍铖宇 庄建军 黄晓林 侯凤贞 宁新宝 
国家自然科学基金(批准号:60701002);江苏省自然科学基金(批准号:BK2011565);江苏省“六大人才高峰”高层次人才项目(批准号:2011-DZXX-035)资助的课题~~
在心率变异性的非线性分析中,Poincare散点图分析是一种重要手段.本文基于Poincare差值散点图(modified Poincare plot)提出了两个参数—区域分布熵和区域分布系数,用于定量描述所考察区域内散点的分布趋势,并提出对散点在4个象限中的...
关键词：心率变异性 Poincare差值散点图 象限 
全选清除导出
共2页<12>
检索报告 对象比较 聚类工具 使用帮助 返回顶部