作者投稿和查稿 主编审稿 专家审稿 编委审稿 远程编辑

计算机工程 ›› 2010, Vol. 36 ›› Issue (22): 46-48. doi: 10.3969/j.issn.1000-3428.2010.22.016

• 软件技术与数据库 • 上一篇    下一篇

基于FeaVer的MINIX 3验证和改进

全嘉辉,张欢欢   

  1. (华东理工大学信息科学与工程学院,上海 200237)
  • 出版日期:2010-11-20 发布日期:2010-11-18
  • 作者简介:全嘉辉(1984-),男,硕士研究生,主研方向:形式化方法,分布式系统,操作系统;张欢欢,副教授
  • 基金资助:
    国家自然科学基金资助项目(60703026);广东省教育部产学研合作基金资助项目(2007A090601001)

Verification and Improvement of MINIX 3 Based on FeaVer

QUAN Jia-hui, ZHANG Huan-huan   

  1. (School of Information Science and Engineering, East China University of Science and Technology, Shanghai 200237, China)
  • Online:2010-11-20 Published:2010-11-18

摘要: 使用FeaVer对MINIX 3文件系统源代码进行形式化验证,并找到其中的错误代码。在验证的过程中引入测试用具的概念,它的特点是高效性和可复用性。在验证结果的基础上对原来的验证模型进行修改,并建立新的模型。经验证新模型符合应有的正确性属性。以新模型为依据对MINIX 3的源代码进行改进,使操作系统达到一个更可靠的状态。

关键词: 形式化验证, 模型检测, MINIX 3操作系统, 文件系统

Abstract: FeaVer is used to perform a formal verification of source codes of MINIX 3 file system, and the error codes are found. In the procedure of verification, the concept of test harness is introduced, whose characteristics are efficient and reproducible. The original model based on the verification results is modified and a new model is built. It is verified that the new model conforms to the correctness property specified. The source files of MINIX 3 are upgraded according to the new model to make the operating system more reliable.

Key words: formal verification, model check, MINIX 3 operating system, file system

中图分类号: