μcos-ⅲ任务调度器的验证

《μcos-ⅲ任务调度器的验证》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、睡t霉(代、)中国科学技术大学硕士学位论lJLC／oS．III任务调度器的验证作者姓名：学科专业：导师姓名：完成时间：罗尔聪计算机软件与理论邵中教授郭宇副教授二O一四年六月二日文UniVerSityofScienceandTechnoIogyofChinaAdiSSertlatiOnfIormaSter’SdegreeV6rifiCatiOnofpC／OS-¨IT_aSkSChedUIerAumor’sName：Special匆：SupeⅣisor：Fillishedtime：ErcongLuOConlputerSo胁areandTheo巧Pro￡Zhong

2、ShaoA．P．Yu(mo№e2矾，2014’中国科学技术大学学位论文原创性声明本人声明所呈交的学位论文，是本人在导师指导下进行研究工作所取得的成果。除已特别加以标注和致谢的地方外，论文中不包含任何他人已经发表或撰写过的研究成果。与我一同工作的同志对本研究所做的贡献均己在论文中作了明确的说明。作者签名：!至塾!薹：签字日期：兰三丝垡!堡垒旦中国科学技术大学学位论文授权使用声明作为申请学位的条件之一，学位论文著作权拥有者授权中国科学技术大学拥有学位论文的部分使用权，即：学校有权按有关规定向国家有关部门或机构送交论文的复印件和电子版，允许论文被查阅和借阅，可以将

3、学位论文编入《中国学位论文全文数据库》等有关数据库进行检索，可以采用影印、缩印或扫描等复制手段保存、汇编学位论文。本人提交的电子文档的内容和纸质论文的内容相一致。保密的学位论文在解密后也遵守此规定。吨么开口保密(——年)作者签名：、琴糸雏．作者签名：至!：墅：签字日期：垄!生年苎塑堑旦导师答名：匿蔓室@)签字日期：立．丛1堑．S：；!摘要近年来随着嵌入式设备的日益普及，嵌入式软件的安全性越发显得重要。在一些关键领域，如航天、医疗、军事、核能等，如果嵌入式软件存在程序漏洞，有可能导致程序在非正常状态运行，从而会带来灾难性的后果。为了解决这一类的可靠性问题，传统

4、软件开发者通常会采用软件测试的方法去发现程序错误。但是，软件测试无法保证整个系统完全不存在缺陷。程序验证探寻一条逻辑验证为基础的解决软件安全性的道路。程序验证能够克服软件测试的一些固有缺点，能够证明程序严格地符合一定的性质，从而保证软件的可靠性。操作系统中的任务调度器由于其结构复杂而难以验证：首先任务调度器的代码涉及到诸多的复杂内核数据结构，在验证它们之前需要描述这部分内核数据结构的性质和它们相互之间应该满足的复杂关系；此外在任务调度过程中，内核需要保证调度策略的正确性，即选取具有最高优先级的就绪任务，然后通过任务上下文切换来保证高优先级的任务优先得到运行。

5、本文以屺／0S—III内核中的任务调度器为研究对象，选取与调度有关的核心代码，验证调度器代码满足优先调度最高优先级任务的性质。本文基于分离逻辑与SCAP验证理论，利用Coq辅助证明工具，通过定义机器模型、操作语义、逻辑断言以及推导规则等来构建验证框架。在验证框架，本文定义了内核数据结构和“优先调度最高优先级”的性质的逻辑描述，模块化地对内核代码进行推理，最终的验证结果保证此／OS—III任务调度器的满足可靠性的要求。本文主要贡献如下：(1)验证了此／0S—III任务调度器中的核心代码满足以下的关键性质：A．内存安全性、B．代码的功能正确性和c．优先调度最高优

6、先级任务；(2)在证明辅助工具coq中实现了整个验证框架和调度器核心代码的验证过程，所有定义和证明都可以接受机器的自动检查。关键词：任务调度器形式化验证分离逻辑coq证明工具最高优先级摘要IIAbstractABSTRACTIIlrecentyears，enmeddcddeVicesarebecomingmoreandmorepopul瓯andthlepotentialriskshiddenille力a_b甜dedso脚areareincreasiIl哲ypfoIIlinent．Ifenlbeddedpro铲ams谢恤bugsareeXecutedinkey

7、areas，itmayleadtodisas仃ousconsequences．Peoplecheckerrolrsand矗xt11eIn证舰ditionalsofhⅣareen罢：inee血19mroughsoftwaretesting．HoweVer，sof啊aretestiI培camlotgIlar跚teematmeprogr锄shaVenodefect．BasodonforInalIo百c，programveri丘cationeXploresa110merwayfore11毗gsafety．Pm伊锄v耐fication孙的idst11eirlheren

8、tdr剐沌ackmotedinsofhvareteS