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

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

    44            King's College London, United Kingdom}

    44            King's College London, United Kingdom}

    45 \maketitle

    45 \maketitle

    46 

    46 

    47 \begin{abstract}

    47 \begin{abstract}

    49 processes with priorities, one faces the problem of priority

    49 processes with priorities, one faces the problem of priority

    50 inversion. This problem can make the behaviour of processes

    50 inversion. This problem can make the behaviour of processes

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

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

    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

    61 efficiently implement this protocol. Earlier correct implementations

    61 efficiently implement this protocol. Earlier correct implementations

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

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

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

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

    64 

    64 

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

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

    67 \end{abstract}

    67 \end{abstract}

    68 

    68 

    69 \input{session}

    69 \input{session}

    70 

    70 

    71 \bibliographystyle{plain}

    71 \bibliographystyle{plain}