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

Formal Verification of Priority Ceiling Protocol

作　　者：张博颖[1,2] 

机构地区：[1]中国科学院软件研究所计算机科学重点实验室 [2]中国科学院研究生院,北京100039

出　　处：《计算机仿真》2007年第6期276-279,共4页Computer Simulation

基　　金：国家863计划项目(2004AA412040);国家自然科学基金项目(60373055;60374058)

摘　　要：优先级顶协议是一种优先级驱动的抢占式调度协议,它具有无死锁和单阻塞的性质。Dang Van Hung和Philip Chan在文献[6]中形式地规范和验证了这两个性质。但他们没有对状态函数HiPripcp明确定义,这使得验证的细节较难理解。为了解决这个问题,提出了一种新的方法来验证优先级顶协议单阻塞的性质。通过时段演算的方法,对优先级顶协议进行了规范,并给出了状态函数HiPripcp的明确定义。根据优先级顶协议的规范,形式地验证了该协议的单阻塞性质。采用的验证方法更少地依赖于HiPripcp,这使得验证的细节更易于理解。此外,提出的验证方法可被应用于实时数据库系统中类似协议的形式化验证。Priority ceiling protocol is a priority - driven preemptive protocol, it avoids deadlocks and guarantees that any task is blocked at most once. Dang Van Hung and Philip Chan [6] formally specified and verified both properties in [6]. In their proof, the state function HiPripcp is not defined explicitly, which makes the proof details hard to follow. To solve this problem, a new approach is presented to verify the blocked at most once property of this protocol. With duration calculus, we specify the priority ceiling protocol and give a specific definition to HiPripcp. From the specification, we formally verify the properties of this protocol. Our approach relies less on HiPripcp, this makes the proof details easy to follow. Further, this approach can be used to verify the similar properties of protocols of real - time database systems.

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

分 类 号：TP301[自动化与计算机技术—计算机系统结构] TP316[自动化与计算机技术—计算机科学与技术]