科研之友
微信
新浪微博
Facebook
分享链接
摘要
本发明公开了一种基于边界模型检测技术的微内核操作系统接口的形式化验证方法。首先从微内核操作系统规范中提取微内核API的性质,把性质抽象为一阶逻辑公式；并将程序要满足的基本性质从通用基本性质库提取其一阶逻辑公式；微内核操作系统待验证的API从源代码中提取出来,包括相关的数据结构和内部调用的函数；将提取的微内核API分别和微内核API性质、通用性质进行合并获得含有API性质的微内核API、含有通用性质的微内核API；分别对两个API程序进行抽象建模,获得一阶逻辑公式；最后应用SMT求解器验证,如果验证失败,则根据验证公式给出的错误提示修改微内核API代码并重新验证,直到验证通过,说明该接口程序满足性质。
- 单位
