1 \documentclass[runningheads]{llncs}

     1 \documentclass[runningheads]{llncs}

     2 \usepackage{isabelle}

     2 \usepackage{isabelle}

     3 \usepackage{isabellesym}

     3 \usepackage{isabellesym}

     4 \usepackage{amsmath}

     4 \usepackage{amsmath}

     5 \usepackage{amssymb}

     5 \usepackage{amssymb}

     6 %\usepackage{tikz}

     7 %\usepackage{tikz}

     7 %\usepackage{pgf}

     8 %\usepackage{pgf}

     8 %\usetikzlibrary{arrows,automata,decorations,fit,calc}

     9 %\usetikzlibrary{arrows,automata,decorations,fit,calc}

     9 %\usetikzlibrary{shapes,shapes.arrows,snakes,positioning}

    10 %\usetikzlibrary{shapes,shapes.arrows,snakes,positioning}

    10 %\usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf

    11 %\usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf

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

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

    43            King's College London, United Kingdom}

    44            King's College London, United Kingdom}

    44 \maketitle

    45 \maketitle

    45 

    46 

    46 \begin{abstract}

    47 \begin{abstract}

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

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

    51 Priority Inheritance Protocol is one solution implemented in many

    52 Priority Inheritance Protocol is one solution implemented in many

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

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

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

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

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

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

    60 efficiently implement this protocol. Earlier correct implementations

    61 efficiently implement this protocol. Earlier correct implementations

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

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

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

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

    63 

    64 

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

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

    66 \end{abstract}

    67 \end{abstract}

    67 

    68 

    68 \input{session}

    69 \input{session}

    69 

    70 

    70 \bibliographystyle{plain}

    71 \bibliographystyle{plain}