\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{Myhill-Nerode using Regular Expressions}


\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
processes involving 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 the priority inversion problem, but the correctness of this solution has never
been formally verified in a theorem prover. The original description
of the Property Inheritance Protocol presents a ``correctness proof''
done with pencil-and-paper for an \emph{incorrect} algorithm. This has
already been pointed out in the literature. In this paper we fix the
problem of the original proof by making all notions precise and implement 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: