Institutional Repository
| 优先级顶协议的形式规范和验证 | |
| 张博颖 | |
| 2006-06-02 | |
| Degree Grantor | 中国科学院软件研究所 |
| Degree Level | 博士 |
| Place of Degree Grantor | 软件研究所 |
| Keyword | 优先级顶协议 时段演算 调度 实时操作系统 形式规范和验证 |
| English Abstract | 抢占式实时操作系统中的任务在争夺共享资源时会引起死锁和优先级反转，它们会降低系统的可调度性。优先级顶协议是一种优先级驱动的抢占式调度协议，它能够避免死锁和限制优先级反转不超过单个关键段的执行时间。Dang Van Hung和Philip Chan[6]使用时段演算的方法，形式地规范和验证了优先级顶协议的无死锁和单阻塞性质。但是[6]没有对状态函数HiPripcp明确定义，却在验证优先级顶协议的性质时非常依赖于HiPripcp，这使得证明的细节较难理解。 本文在[6]的基础上，使用时段演算的方法对优先级顶协议重新进行了规范，并给出了验证该协议性质的一种新方法。本文的主要工作包括以下几点： 1、修改了[6]中实时操作系统环境的一些形式规范，并且补充了一些新的规范，这使得环境模型更加准确。 2、给出了使用一类协议的调度器模型，这类协议都允许优先级反转。 3、对状态函数HiPripcp进行了明确的定义，并且形式地证明了HiPripcp的性质。 4、根据HiPripcp的定义，对优先级顶协议单阻塞的性质进行了重新证明。我们采用的证明方法完全不同于[6]，而且证明的细节更易于理解。 5、证明了PCP能够避免传递的阻塞，这保证了HiPripcp是良定义的。 最后，本文针对优先级顶协议单阻塞性质的新验证方法可被应用于实时数据库系统中类似协议性质的验证。 |
| Pages | 49 |
| Language | 中文 |
| Content Type | 学位论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/7552 |
| Collection | 中科院软件所_中科院软件所 |
| Recommended Citation GB/T 7714 | 张博颖. 优先级顶协议的形式规范和验证[D]. 软件研究所. 中国科学院软件研究所,2006. |
| Files in This Item: | ||||||
| File Name/Size | DocType | Version | Access | License | ||
| 10001_20032801500434（378KB） | 限制开放 | -- | Application Full Text | |||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment