35 \newcommand{\isasymbigplus}{\ensuremath{\bigplus}}

    35 \newcommand{\isasymbigplus}{\ensuremath{\bigplus}}

    36 

    36 

    37 \newcommand{\bigplus}{\mbox{\Large\bf$+$}}

    37 \newcommand{\bigplus}{\mbox{\Large\bf$+$}}

    38 \begin{document}

    38 \begin{document}

    39 

    39 

    42 \author{Xingyuan Zhang\inst{1} \and Christian Urban\inst{2} \and Chunhan Wu\inst{1}}

    41 \author{Xingyuan Zhang\inst{1} \and Christian Urban\inst{2} \and Chunhan Wu\inst{1}}

    43 \institute{PLA University of Science and Technology, China \and 

    42 \institute{PLA University of Science and Technology, China \and 

    44            King's College London, United Kingdom}

    43            King's College London, United Kingdom}

    45 \maketitle

    44 \maketitle

    46 

    45 

    55 pointed out in the literature, the original informal investigation of

    54 pointed out in the literature, the original informal investigation of

    56 the Property Inheritance Protocol presents a correctness ``proof'' for

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

    57 an \emph{incorrect} algorithm. In this paper we fix the problem of

    56 an \emph{incorrect} algorithm. In this paper we fix the problem of

    58 this proof by making all notions precise and implementing a variant of

    57 this proof by making all notions precise and implementing a variant of

    59 a solution proposed earlier. Our formalisation in Isabelle/HOL

    58 a solution proposed earlier. Our formalisation in Isabelle/HOL

    61 efficiently implement this protocol. Earlier correct implementations

    60 efficiently implement this protocol. Earlier correct implementations

    62 were criticised as too inefficient. Our formalisation is based on

    61 were criticised as too inefficient. Our formalisation is based on

    63 Paulson's inductive approach to verifying protocols.\medskip

    62 Paulson's inductive approach to verifying protocols.\medskip

    64 

    63 

    65 {\bf Keywords:} Priority Inheritance Protocol, formal connectness proof, 

    64 {\bf Keywords:} Priority Inheritance Protocol, formal connectness proof,