朱晓冉

作品数：3被引量：16H指数：2
导出分析报告
供职机构：华东师范大学更多>>
发文主题：操作系统定理证明智能卡操作系统内核循环不变式更多>>
发文领域：自动化与计算机技术电子电信更多>>
发文期刊：《信息网络安全》《软件学报》《计算机工程与科学》更多>>
所获基金：国家自然科学基金上海市科学技术委员会资助项目国家重点基础研究发展计划更多>>
-
在结果中检索

检索结果分析

署名顺序

  • 全部
  • 第一作者
结果分析中...
共 条 记 录，以下是1-3
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
嵌入式实时操作系统内核混合代码的自动化验证框架被引量：12
《软件学报》2020年第5期1353-1373,共21页郭建 丁继政 朱晓冉 
国家自然科学基金(61532019);上海市重点项目(19511103602)。
"如何构造高可信的软件系统"已成为学术界和工业界的研究热点.操作系统内核作为软件系统的基础组件,其安全可靠是构造高可信软件系统的重要环节.为了确保操作系统内核的安全可靠,将形式化方法引入到操作系统内核验证中,提出了一个自动...
关键词：实时操作系统 VCC 混合程序验证 自动验证 Z3求解器 
基于Event-B方法的多应用智能卡的建模与开发被引量：2
《计算机工程与科学》2014年第10期1943-1951,共9页章玥 郭建 朱晓冉 王文君 朱晶洋 汤家华 陈峻念 
国家自然科学基金资助项目(91118008);国家973计划资助项目(2011CB302904);上海市科委资助项目(12511504205);信息网络安全公安部重点实验室开放课题资助项目(C12604);上海高校知识服务平台-可信物联网产学研联合研发中心(筹)资助项目
Event-B是一种基于集合论和谓词逻辑的形式化系统语言,能够采用精化策略为系统建立逐渐精化的模型。提出了如何将Event-B应用到实际工业领域的方法,包括重写需求、建立抽象模型及逐层精化三个步骤。首先从环境、功能、性质三个主要方面...
关键词：智能卡 EVENT-B 精化 定理证明 
基于模型的开发方法在多应用智能卡中的应用被引量：2
《信息网络安全》2013年第12期75-79,共5页章玥 郭建 朱晓冉 
上海市科委项目[12511504205];信息网络安全公安部重点实验室开放课题[C12604]
安全性、可靠性是嵌入式软件的重要性质。为了更好地保证开发的嵌入式软件是可靠和安全的,提出了一种基于模型的开发方法学,包括提炼需求、建立抽象模型及逐层精化三个步骤。首先从环境、功能、性质三个主要方面提取需求,同时明确层次...
关键词：智能卡 Event—B 形式化方法 定理证明 
全选清除导出
共1页<1>
检索报告 对象比较 聚类工具 使用帮助 返回顶部