- 1
- 2
- 3
- 4
- 5
微内核架构内存管理的形式化设计和验证方法研究
资料介绍
由于巨大的规模和复杂性,操作系统的设计和实现的正确性很难用传统的定量方法来描述.本文阐述对微内核操作系统的形式化设计和验证的方法.在汇编层利用非确定性自动机对系统进行形式化建模,并使用Hoare三元组描述模块接口函数的前后置条件,作为函数正确性的定义.以实现的VSOS(Verified Secure Operating System)内存管理模块为例,在Isabelle/HOL定理证明器环境中对建立的内存管理模型和系统行为的操作语义进行形式化描述,并对内存管理模块的设计和实现的正确性进行验证.结果表明,这一方法是可行的和高效的.
部分文件列表
文件名 | 大小 |
微内核架构内存管理的形式化设计和验证方法研究.pdf | 1M |
部分页面预览
(完整内容请下载后查看)最新上传
-
21ic小能手 打赏10.00元 2天前
-
21ic小能手 打赏10.00元 2天前
-
cai0603 打赏3.00元 3天前
用户:CJQ_ENJOY
-
21ic小能手 打赏5.00元 3天前
-
21ic小能手 打赏10.00元 3天前
-
cai0603 打赏3.00元 3天前
用户:dongshao
-
21ic小能手 打赏5.00元 3天前
-
21ic小能手 打赏10.00元 3天前
-
21ic下载 打赏310.00元 3天前
用户:gsy幸运
-
21ic下载 打赏310.00元 3天前
用户:zhengdai
-
21ic下载 打赏310.00元 3天前
用户:小猫做电路
-
21ic下载 打赏310.00元 3天前
用户:liqiang9090
-
21ic下载 打赏270.00元 3天前
用户:kk1957135547
-
21ic下载 打赏160.00元 3天前
用户:w178191520
-
21ic下载 打赏160.00元 3天前
用户:w1966891335
-
21ic下载 打赏50.00元 3天前
用户:w993263495
-
21ic下载 打赏40.00元 3天前
用户:w993263495
-
21ic下载 打赏90.00元 3天前
用户:cooldog123pp
-
21ic下载 打赏30.00元 3天前
用户:sun2152
-
21ic下载 打赏40.00元 3天前
用户:xzxbybd
-
21ic下载 打赏40.00元 3天前
用户:铁蛋锅
-
21ic下载 打赏30.00元 3天前
用户:happypcb
-
21ic下载 打赏50.00元 3天前
用户:forgot
-
21ic下载 打赏10.00元 3天前
用户:xuzhen1
-
21ic下载 打赏20.00元 3天前
用户:wanglu6666
-
21ic下载 打赏5.00元 3天前
用户:人间留客
-
21ic下载 打赏5.00元 3天前
用户:jyxjiyixing
-
21ic下载 打赏5.00元 3天前
用户:akae_du
-
21ic下载 打赏5.00元 3天前
用户:ouyang_56
-
21ic小能手 打赏5.00元 3天前
-
21ic小能手 打赏5.00元 3天前
-
21ic小能手 打赏5.00元 3天前
-
21ic小能手 打赏5.00元 3天前
-
21ic小能手 打赏5.00元 3天前
-
xlhtracy 打赏10.00元 3天前
-
xlhtracy 打赏10.00元 3天前
-
21ic小能手 打赏5.00元 3天前
-
21ic小能手 打赏5.00元 3天前
-
xlhtracy 打赏5.00元 3天前
-
czmhcy 打赏1.00元 3天前
资料:bitboy
全部评论(0)