article · 2007

Formal Verification of Priority Ceiling Protocol

Cited by 0Abstract and details only

Abstract

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.

Cite this paper

APA 7

Bo-ying, Z. (2007). Formal Verification of Priority Ceiling Protocol.

MLA 9

Bo-ying, Zhang. “Formal Verification of Priority Ceiling Protocol.” 2007.

Chicago

Bo-ying, Zhang. 2007. “Formal Verification of Priority Ceiling Protocol.”

Harvard

Bo-ying, Z. (2007) ‘Formal Verification of Priority Ceiling Protocol’.

BibTeX

@article{boying2007formal,
  title = {{Formal Verification of Priority Ceiling Protocol}},
  author = {Bo-ying, Zhang},
  year = {2007}
}

Made from the index record. Check names, capitalisation and page numbers against the paper. Need another style? AI for Research has over 10,000.