\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, University of London, U.K.}
\maketitle

%\mbox{}\\[-10mm]
\begin{abstract}
Despite the wide use of Priority Inheritance Protocol in real time operating
system, it's correctness has never been formally proved and mechanically checked. 
All existing verification are based on model checking technology. Full automatic
verification gives little help to understand why the protocol is correct. 
And results such obtained only apply to models of limited size. 
This paper presents a formal verification based on theorem proving. 
Machine checked formal proof does help to get deeper understanding. We found 
the fact which is not mentioned in the literature, that the choice of next 
thread to take over when an critical resource is release does not affect the correctness
of the protocol. The paper also shows how formal proof can help to construct 
correct and efficient implementation. 
\end{abstract}


\input{session}

%%\mbox{}\\[-10mm]
\bibliographystyle{plain}
\bibliography{root}

\end{document}

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