优先级顶协议的形式化验证

摘要：

优先级顶协议是一种优先级驱动的抢占式调度协议,它具有无死锁和单阻塞的性质.Dang Van Hung 和Philip Chan在文献[6]中形式地规范和验证了这两个性质.但他们没有对状态函数HiPripcp明确定义,这使得验证的细节较难理解.为了解决这个问题,提出了一种新的方法来验证优先级顶协议单阻塞的性质.通过时段演算的方法,对优先级顶协议进行了规范,并给出了状态函数HiPripcp的明确定义.根据优先级顶协议的规范,形式地验证了该协议的单阻塞性质.采用的验证方法更少地依赖于HiPripcp,这使得验证的细节更易于理解.此外,提出的验证方法可被应用于实时数据库系统中类似协议的形式化验证.

关键词：优先级顶协议、时段演算、调度、实时操作系统、形式规范和验证

所属期刊栏目：24

分类号：TP301;TP316(计算技术、计算机技术)

资助基金：国家高技术研究发展计划863计划2004AA412040;国家自然科学基金60373055;60374058

在线出版日期：2007-07-16（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：276-279