52 Priority Inheritance Protocol is one solution implemented in many |
52 Priority Inheritance Protocol is one solution implemented in many |
53 systems for solving this problem, but the correctness of this solution |
53 systems for solving this problem, but the correctness of this solution |
54 has never been formally verified in a theorem prover. As already |
54 has never been formally verified in a theorem prover. As already |
55 pointed out in the literature, the original informal investigation of |
55 pointed out in the literature, the original informal investigation of |
56 the Property Inheritance Protocol presents a correctness ``proof'' for |
56 the Property Inheritance Protocol presents a correctness ``proof'' for |
57 an \emph{incorrect} algorithm. In this paper we fix the problem of the |
57 an \emph{incorrect} algorithm. In this paper we fix the problem of |
58 original proof by making all notions precise and implementing a |
58 this proof by making all notions precise and implementing a variant of |
59 variant of a solution proposed earlier. Our formalisation in |
59 a solution proposed earlier. Our formalisation in Isabelle/HOL |
60 Isabelle/HOL uncovered facts not mentioned in the literature, but also |
60 uncovered facts not mentioned in the literature, but also shows how to |
61 shows how to efficiently implement this protocol. Earlier correct |
61 efficiently implement this protocol. Earlier correct implementations |
62 implementations were criticised as too inefficient. Our formalisation |
62 were criticised as too inefficient. Our formalisation is based on |
63 is based on Paulson's inductive approach to verifying |
63 Paulson's inductive approach to verifying protocols.\medskip |
64 protocols.\medskip |
|
65 |
64 |
66 {\bf Keywords:} Priority Inheritance Protocol, formal connectness proof, |
65 {\bf Keywords:} Priority Inheritance Protocol, formal connectness proof, |
67 realtime systems |
66 realtime systems |
68 \end{abstract} |
67 \end{abstract} |
69 |
68 |