郭建

作品数:2被引量:12H指数:1
导出分析报告
供职机构:教育部更多>>
发文主题:Z3VCC系统内核求解器嵌入式实时操作更多>>
发文领域:自动化与计算机技术更多>>
发文期刊:《微纳电子与智能制造》《软件学报》更多>>
所获基金:国家自然科学基金更多>>
-

检索结果分析

署名顺序

  • 全部
  • 第一作者
结果分析中...
条 记 录,以下是1-2
视图:
排序:
嵌入式实时操作系统内核混合代码的自动化验证框架被引量:12
《软件学报》2020年第5期1353-1373,共21页郭建 丁继政 朱晓冉 
国家自然科学基金(61532019);上海市重点项目(19511103602)。
"如何构造高可信的软件系统"已成为学术界和工业界的研究热点.操作系统内核作为软件系统的基础组件,其安全可靠是构造高可信软件系统的重要环节.为了确保操作系统内核的安全可靠,将形式化方法引入到操作系统内核验证中,提出了一个自动...
关键词:实时操作系统 VCC 混合程序验证 自动验证 Z3求解器 
基于在线模型检验技术的微内核验证
《微纳电子与智能制造》2020年第1期102-109,共8页董星河 郭建 
自然科学基金委重点项目(61532019);上海市重点项目(19511103602)资助。
物联网的兴起,对操作系统的可靠性提出了更高的要求。为确保微内核操作系统的安全性,提出了一种基于事件总线的微内核在线模型验证框架,主要思想是通过映射函数将源代码转换成抽象模型,并从微内核规范中抽取性质。根据源代码的控制流程...
关键词:操作系统 有界模型检查 映射函数 线性时态逻辑 
检索报告 对象比较 聚类工具 使用帮助 返回顶部