期刊导航
期刊开放获取
河南省图书馆
退出
期刊文献
+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
检索
高级检索
期刊导航
共找到
2
篇文章
<
1
>
每页显示
20
50
100
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
显示方式:
文摘
详细
列表
相关度排序
被引量排序
时效性排序
高阶逻辑验证系统HOL及其应用初探
1
作者
陈波
《科技视界》
2018年第28期162-163,共2页
形式化方法在硬件、软件的设计和验证中的应用越来越广泛,基于不同理论的形式化验证工具应运而生。本文对形式化验证工具定理证明系统HOL作了介绍,并结合例子说明HOL系统在硬件设计中的应用。
关键词
形式化验证方法
hol
逻辑
hol
系统
带复位的奇偶校验器
下载PDF
职称材料
基于Isabelle/HOL的安全操作系统形式化验证方法
2
作者
郭毅
杨维永
刘苇
《计算机与现代化》
2017年第4期99-104,共6页
操作系统作为信息时代的基石,其安全性不言而喻。常规的软件测试方法不足以保障操作系统的安全性,需使用更为严格的基于数理逻辑的形式化验证方法。本文提出一种软件形式化验证的新思路:通过在Isabelle中构造模拟运行环境,使汇编代码运...
操作系统作为信息时代的基石,其安全性不言而喻。常规的软件测试方法不足以保障操作系统的安全性,需使用更为严格的基于数理逻辑的形式化验证方法。本文提出一种软件形式化验证的新思路:通过在Isabelle中构造模拟运行环境,使汇编代码运行其中,并记录系统状态的变化,最终根据程序运行前后系统状态的变化情况判断程序的正确性和安全性。重点介绍了顺序、分支和循环等3种程序结构的证明方法,并通过一个程序实例证明,得到在任意前提条件下程序执行前后系统状态的变化情况。
展开更多
关键词
安全操作系统
形式化验证
Isabelle/
hol
霍尔逻辑
下载PDF
职称材料
题名
高阶逻辑验证系统HOL及其应用初探
1
作者
陈波
机构
山东理工大学计算机科学与技术学院
出处
《科技视界》
2018年第28期162-163,共2页
文摘
形式化方法在硬件、软件的设计和验证中的应用越来越广泛,基于不同理论的形式化验证工具应运而生。本文对形式化验证工具定理证明系统HOL作了介绍,并结合例子说明HOL系统在硬件设计中的应用。
关键词
形式化验证方法
hol
逻辑
hol
系统
带复位的奇偶校验器
Keywords
Formal Verification method
hol logic
hol
system
Parity- reset checking device
分类号
TP316 [自动化与计算机技术—计算机软件与理论]
TP309 [自动化与计算机技术—计算机系统结构]
下载PDF
职称材料
题名
基于Isabelle/HOL的安全操作系统形式化验证方法
2
作者
郭毅
杨维永
刘苇
机构
南京南瑞信息通信科技有限公司
出处
《计算机与现代化》
2017年第4期99-104,共6页
基金
国家自然科学基金资助项目(61321491)
江苏省工业和信息产业转型升级专项项目(2015SJXKJ5038)
国网电力科学研究院科技项目(5246DR150002)
文摘
操作系统作为信息时代的基石,其安全性不言而喻。常规的软件测试方法不足以保障操作系统的安全性,需使用更为严格的基于数理逻辑的形式化验证方法。本文提出一种软件形式化验证的新思路:通过在Isabelle中构造模拟运行环境,使汇编代码运行其中,并记录系统状态的变化,最终根据程序运行前后系统状态的变化情况判断程序的正确性和安全性。重点介绍了顺序、分支和循环等3种程序结构的证明方法,并通过一个程序实例证明,得到在任意前提条件下程序执行前后系统状态的变化情况。
关键词
安全操作系统
形式化验证
Isabelle/
hol
霍尔逻辑
Keywords
secure operating system
formal verification
Isabelle/
hol
Hoare
logic
分类号
TP309.2 [自动化与计算机技术—计算机系统结构]
下载PDF
职称材料
题名
作者
出处
发文年
被引量
操作
1
高阶逻辑验证系统HOL及其应用初探
陈波
《科技视界》
2018
0
下载PDF
职称材料
2
基于Isabelle/HOL的安全操作系统形式化验证方法
郭毅
杨维永
刘苇
《计算机与现代化》
2017
0
下载PDF
职称材料
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
上一页
1
下一页
到第
页
确定
用户登录
登录
IP登录
使用帮助
返回顶部