\documentclass[runningheads]{llncs}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage{amsmath}
\usepackage{amssymb}
%\usepackage{tikz}
%\usepackage{pgf}
%\usetikzlibrary{arrows,automata,decorations,fit,calc}
%\usetikzlibrary{shapes,shapes.arrows,snakes,positioning}
%\usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf
%\usetikzlibrary{matrix}
\usepackage{pdfsetup}
\usepackage{ot1patch}
\usepackage{times}
%%\usepackage{proof}
%%\usepackage{mathabx}
\usepackage{stmaryrd}
\usepackage{url}

\titlerunning{Proving the Priority Inheritance Protocol Correct}


\urlstyle{rm}
\isabellestyle{it}
\renewcommand{\isastyleminor}{\it}%
\renewcommand{\isastyle}{\normalsize\it}%


\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
\renewcommand{\isasymequiv}{$\dn$}
\renewcommand{\isasymemptyset}{$\varnothing$}
\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}

\newcommand{\isasymcalL}{\ensuremath{\cal{L}}}
\newcommand{\isasymbigplus}{\ensuremath{\bigplus}}

\newcommand{\bigplus}{\mbox{\Large\bf$+$}}
\begin{document}

\title{A Formalisation of Priority Inheritance Protocol \\ 
       for Correct and Efficient Implementation}
\author{Xingyuan Zhang\inst{1} \and Christian Urban\inst{2} \and Chunhan Wu\inst{1}}
\institute{PLA University of Science and Technology, China \and 
           King's College London, United Kingdom}
\maketitle

\begin{abstract}
In realtime systems with support for resource locking and for
processes with priorities, one faces the problem of priority
inversion. This problem can make the behaviour of processes
unpredictable and the resulting bugs can be hard to find.  The
Priority Inheritance Protocol is one solution implemented in many
systems for solving this problem, but the correctness of this solution
has never been formally verified in a theorem prover. As already
pointed out in the literature, the original informal investigation of
the Property Inheritance Protocol presents a correctness ``proof'' for
an \emph{incorrect} algorithm. In this paper we fix the problem of the
original proof by making all notions precise and implementing a
variant of a solution proposed earlier. Our formalisation in
Isabelle/HOL uncovered facts not mentioned in the literature, but also
shows how to efficiently implement this protocol. Earlier correct
implementations were criticised as too inefficient. Our formalisation
is based on Paulson's inductive approach to verifying
protocols.\medskip

{\bf Keywords:} Priority Inheritance Protocol, formal connectness proof, 
realtime systems
\end{abstract}

\input{session}

\bibliographystyle{plain}
\bibliography{root}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: