\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

this 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: