--- a/prio/Paper/document/root.tex	Fri Jan 27 13:50:02 2012 +0000
+++ b/prio/Paper/document/root.tex	Fri Jan 27 23:19:10 2012 +0000
@@ -41,28 +41,34 @@
        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, U.K.}
+           King's College London, United Kingdom}
 \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. 
+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}
 
-%%\mbox{}\\[-10mm]
 \bibliographystyle{plain}
 \bibliography{root}