资料下载
×
操作系统汇编级形式化设计和验证方法
消耗积分:3 |
格式:rar |
大小:1.77 MB |
2018-01-05
分享资料个
由于系统的巨大规模，操作系统设计和实现的正确性很难用传统的方法进行描述和验证．在汇编层形式化地对系统模块的功能语义进行建模，提出一种汇编级的系统状态模型，作为汇编语言层设计和验证的纽带．通过定义系统状态模型的合法状态和状态转换函数来建立系统状态模型的论域，并以此来描述汇编层的论域．通过验证汇编层的功能模块的正确性来保证汇编语言层设计的正确性，达到对系统功能实现的正确性验证．同时，使用定理证明工具Isabelle/HOL来形式化地描述这一系统状态模型，基于这一形式化模型，在Isabelle/HOL中验证系统模块的功能语义的正确性．以实现的安全可信OS（verifed secure operating system，简称VSOS）为例，阐述了所提出的形式化设计和验证方法。说明了这一方法的可行性．
声明：本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人，不代表电子发烧友网立场。文章及其配图仅供工程师学习之用，如有内容侵权或者其他违规问题，请联系本站处理。 举报投诉
评论(0)
发评论
- 相关下载
- 相关文章
