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

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

Formal Verification of Priority Ceiling Protocol

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.