| 优先级顶协议的形式规范和验证 |
| 张博颖
|
| 2006-06-02
|
| 学位授予单位 | 中国科学院软件研究所
|
| 学位 | 博士
|
| 学位授予地点 | 软件研究所
|
| 关键词 | 优先级顶协议
时段演算
调度
实时操作系统
形式规范和验证
|
| 摘要 | 抢占式实时操作系统中的任务在争夺共享资源时会引起死锁和优先级反转，它们会降低系统的可调度性。优先级顶协议是一种优先级驱动的抢占式调度协议，它能够避免死锁和限制优先级反转不超过单个关键段的执行时间。Dang Van Hung和Philip Chan[6]使用时段演算的方法，形式地规范和验证了优先级顶协议的无死锁和单阻塞性质。但是[6]没有对状态函数HiPripcp明确定义，却在验证优先级顶协议的性质时非常依赖于HiPripcp，这使得证明的细节较难理解。
本文在[6]的基础上，使用时段演算的方法对优先级顶协议重新进行了规范，并给出了验证该协议性质的一种新方法。本文的主要工作包括以下几点：
1、修改了[6]中实时操作系统环境的一些形式规范，并且补充了一些新的规范，这使得环境模型更加准确。
2、给出了使用一类协议的调度器模型，这类协议都允许优先级反转。
3、对状态函数HiPripcp进行了明确的定义，并且形式地证明了HiPripcp的性质。
4、根据HiPripcp的定义，对优先级顶协议单阻塞的性质进行了重新证明。我们采用的证明方法完全不同于[6]，而且证明的细节更易于理解。
5、证明了PCP能够避免传递的阻塞，这保证了HiPripcp是良定义的。
最后，本文针对优先级顶协议单阻塞性质的新验证方法可被应用于实时数据库系统中类似协议性质的验证。 |
| 页数 | 49
|
| 语种 | 中文
|
| 内容类型 | 学位论文
|
| URI标识 | http://ir.iscas.ac.cn/handle/311060/7552
|
| 专题 | 中科院软件所_中科院软件所
|
推荐引用方式
GB/T 7714 |
张博颖. 优先级顶协议的形式规范和验证[D]. 软件研究所. 中国科学院软件研究所,2006.
|
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论