| 复杂内核数据结构程序形式化验证 |
| |
| 引用本文： | 李薛剑,余韵.复杂内核数据结构程序形式化验证[J].计算机系统应用,2023,32(11):253-266. |
| |
| 作者姓名： | 李薛剑 余韵 |
| |
| 作者单位： | 安徽大学 计算机科学与技术学院, 合肥 230601 |
| |
| 摘 要： | 操作系统内核作为软件系统的基础组件, 其安全可靠是构造高可信软件系统的重要环节, 但是, 在实际的验证工作中, 操作系统内核中全局性质的不变式定义, 复杂数据结构程序的形式化描述和验证仍存在很多困难. 本文针对操作系统内核中满足的全局性质, 在代码层以函数为单位, 用全局不变式进行定义, 并在不同的函数中进行形式化验证, 从而证明各个函数符合操作系统内核的全局性质; 针对操作系统内核中经常使用的复杂数据结构程序, 本文通过扩展形状图理论, 提出一种使用嵌套形状图逻辑的方法来形式化描述复杂数据结构程序, 并对该方法进行了正确性证明, 最终成功验证操作系统内核中关于任务创建与调度, 消息队列创建与操作相关的代码.
|
| 关 键 词： | 形式化验证 内核验证 内核数据结构 霍尔逻辑 |
| 收稿时间： | 2023/3/29 0:00:00 |
| 修稿时间： | 2023/5/17 0:00:00 |
Formal Verification of Complex Kernel Data Structure Programs |
| |
| LI Xue-Jian,YU Yun.Formal Verification of Complex Kernel Data Structure Programs[J].Computer Systems& Applications,2023,32(11):253-266. |
| |
| Authors: | LI Xue-Jian YU Yun |
| |
| Affiliation: | School of Computer Science and Technology, Anhui University, Hefei 230601, China |
| |
| Abstract: | |
| |
| Keywords: | formal verification kernel verification kernel data structure Hoare logic |
|
| 点击此处可从《计算机系统应用》浏览原始摘要信息 |
|
点击此处可从《计算机系统应用》下载全文 |
|
