48 In realtime systems with support for resource locking and

    48 In realtime systems with support for resource locking and processes

    49 processes involving priorities, one faces the problem of

    49 involving priorities, one faces the problem of priority

    50 priority inversion. This problem can make the behaviour of processes unpredictable

    50 inversion. This problem can make the behaviour of processes

    51 and the resulting bugs can be hard to find.  The Priority Inheritance

    51 unpredictable and the resulting bugs can be hard to find.  The

    52 Protocol is one solution implemented in many systems for

    52 Priority Inheritance Protocol is one solution implemented in many

    53 solving the priority inversion problem, but the correctness of this solution has never

    53 systems for solving this problem, but the correctness of this solution

    54 been formally verified in a theorem prover. The original description

    54 has never been formally verified in a theorem prover. As already

    55 of the Property Inheritance Protocol presents a ``correctness proof''

    55 pointed out in the literature, the original description of the

    56 done with pencil-and-paper for an \emph{incorrect} algorithm. This has

    56 Property Inheritance Protocol presents an informal correctness

    57 already been pointed out in the literature. In this paper we fix the

    57 ``proof'' for an \emph{incorrect} algorithm. In this paper we fix the

    58 problem of the original proof by making all notions precise and implement a

    58 problem of the original proof by making all notions precise and

    59 variant of a solution proposed earlier. Our formalisation in

    59 implementing a variant of a solution proposed earlier. Our

    60 Isabelle/HOL uncovered facts not mentioned in the literature, but also

    60 formalisation in Isabelle/HOL uncovered facts not mentioned in the

    61 shows how to efficiently implement this protocol. Earlier correct

    61 literature, but also shows how to efficiently implement this

    62 implementations were criticised as too inefficient. Our formalisation  

    62 protocol. Earlier correct implementations were criticised as too

    63 is based on Paulson's inductive approach to verifying 

    63 inefficient. Our formalisation is based on Paulson's inductive

    64 protocols.\medskip

    64 approach to verifying protocols.\medskip