科研之友
微信
新浪微博
Facebook
分享链接
摘要
操作系统内核作为软件系统的基础组件,其安全可靠是构造高可信软件系统的重要环节,但是,在实际的验证工作中,操作系统内核中全局性质的不变式定义,复杂数据结构程序的形式化描述和验证仍存在很多困难.本文针对操作系统内核中满足的全局性质,在代码层以函数为单位,用全局不变式进行定义,并在不同的函数中进行形式化验证,从而证明各个函数符合操作系统内核的全局性质;针对操作系统内核中经常使用的复杂数据结构程序,本文通过扩展形状图理论,提出一种使用嵌套形状图逻辑的方法来形式化描述复杂数据结构程序,并对该方法进行了正确性证明,最终成功验证操作系统内核中关于任务创建与调度,消息队列创建与操作相关的代码.
- 单位
