首页 | 本学科首页   官方微博 | 高级检索  
     

操作系统内核程序函数执行上下文的自动检验
引用本文:汪黎,杨学军,王戟,罗宇.操作系统内核程序函数执行上下文的自动检验[J].软件学报,2007,18(4):1056-1067.
作者姓名:汪黎  杨学军  王戟  罗宇
作者单位:国防科学技术大学,计算机学院,湖南,长沙,410073
基金项目:国家自然科学基金;国家高技术研究发展计划(863计划);教育部跨世纪优秀人才培养计划
摘    要:函数执行上下文正确性是操作系统内核程序最容易违反且难以检查的正确性性质.应用传统的技术检查该类错误都有一定的困难和局限性.提出一个验证函数执行上下文正确性的框架PRPF,详细描述了其建模过程和相关算法.PRPF相比传统技术的优势有:直接检查源代码、无须编写形式化的验证规约、较低的时空运行开销、良好的可扩展性等等.该技术已应用在Linux内核2.4.20的网络设备驱动程序检查中.应用表明,PRPF能够自动探测程序中所有执行路径,有效地检查函数执行上下文的正确性.实验发现了Linux内核的23处编程错误,另有

关 键 词:操作系统内核程序  内核编程接口  程序验证  程序正确性  Linux内核验证
收稿时间:2006-02-24
修稿时间:2006-06-12

Automatedly Checking Function Execution Context of Kernel Programs in Operation Systems
WANG Li,YANG Xue-Jun,WANG Ji and LUO Yu.Automatedly Checking Function Execution Context of Kernel Programs in Operation Systems[J].Journal of Software,2007,18(4):1056-1067.
Authors:WANG Li  YANG Xue-Jun  WANG Ji and LUO Yu
Affiliation:School of Computer, National University of Defense Technology, Changsha 410073, China
Abstract:
Keywords:OS (operation system) kernel programs  kernel programming interfaces  program verification  program correctness  verification of Linux kernel
本文献已被 CNKI 维普 万方数据 等数据库收录!
点击此处可从《软件学报》浏览原始摘要信息
点击此处可从《软件学报》下载全文
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号