\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 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 description of the
Property Inheritance Protocol presents an informal 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: