论文部分内容阅读
抢占式实时操作系统中的任务在争夺共享资源时会引起死锁和优先级反转，它们会降低系统的可调度性。优先级顶协议是一种优先级驱动的抢占式调度协议，它能够避免死锁和限制优先级反转不超过单个关键段的执行时间。Dang Van Hung和Philip Chan[6]使用时段演算的方法，形式地规范和验证了优先级顶协议的无死锁和单阻塞性质。但是没有对状态函数HiPridPCP明确定义，却在验证优先级项协议的性质时非常依赖于HiPriPCP，这使得证明的细节较难理解。
本文在[6]的基础上，使用时段演算的方法对优先级项协议重新进行了规范，并给出了验证该协议性质的一种新方法。本文的主要工作包括以下几点：
·修改了[6]对实时操作系统环境的一些形式规范，并且补充了一些新的规范，这使得环境模型更加准确。
·给出了使用一类协议的调度器模型，这类协议都允许优先级反转。
·对状态函数HiPripcp进行了明确的定义，并且形式地证明了HiPriPCP的性质。
·根据HiPriPCP的定义，对优先级顶协议单阻塞的性质进行了重新证明。本文作者采用的证明方法完全不同于[6]，而且证明的细节更易于理解。
·证明了优先级项协议能够避免传递的阻塞，这保证了HiPriPCP是良定义的。
最后，本文提出的优先级项协议单阻塞性质的验证方法可被应用于实时数据库系统中类似协议性质的验证。