--- a/Journal/document/root.tex	Mon Dec 18 14:52:48 2017 +0000
+++ b/Journal/document/root.tex	Tue Dec 19 14:20:29 2017 +0000
@@ -68,25 +68,26 @@
 \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. We
-also generalise the scheduling problem to the practically relevant case where
-critical sections can overlap. Our formalisation in Isabelle/HOL not
-just uncovers facts not mentioned in the literature, but also helps
-with implementing efficiently this protocol. Earlier correct
-implementations were criticised as too inefficient. Our formalisation
-is based on Paulson's inductive approach to verifying protocols; our
-implementation builds on top of the small PINTOS operating system used
-for teaching.\medskip
+  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. We also generalise the scheduling problem
+  to the practically relevant case where critical sections can
+  overlap. Our formalisation in Isabelle/HOL is based on Paulson's
+  inductive approach to verifying protocols.  The formalisation not
+  only uncovers facts overlooked in the literature, but also helps
+  with an efficient implementation of this protocol. Earlier correct
+  implementations were criticised as too inefficient. Our
+  implementation builds on top of the small PINTOS operating system
+  used for teaching.\medskip
 
 {\bf Keywords:} Priority Inheritance Protocol, formal correctness proof, 
 real-time systems, Isabelle/HOL