--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/document/root.tex	Thu Dec 06 15:12:49 2012 +0000
@@ -0,0 +1,79 @@
+\documentclass[runningheads]{llncs}
+\usepackage{isabelle}
+\usepackage{isabellesym}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage{mathpartir}
+\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}
+\usepackage{color}
+\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{$\_\!\_$}}
+\renewcommand{\isasymiota}{}
+
+\newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}
+\definecolor{mygrey}{rgb}{.80,.80,.80}
+
+\begin{document}
+
+\title{Priority Inheritance Protocol Proved Correct}
+\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 real-time systems with threads, resource locking and 
+priority sched\-uling, one faces the problem of Priority
+Inversion. This problem can make the behaviour of threads
+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
+uncovers 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 correctness proof, 
+real-time systems, Isabelle/HOL
+\end{abstract}
+
+\input{session}
+
+%\bibliographystyle{plain}
+%\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End: