--- a/Journal/document/root.tex Fri Jul 06 22:18:39 2018 +0100
+++ b/Journal/document/root.tex Wed Jan 02 21:09:05 2019 +0000
@@ -1,8 +1,7 @@
%\documentclass{article}
-\documentclass{llncs}
-%\textwidth 130mm
-%\textheight 200mm
-%\renewenvironment{abstract}{\section*{Abstract}\small}{}
+%\documentclass{llncs}
+\documentclass{svjour3}
+
\pagestyle{headings}
\usepackage{isabelle}
\usepackage{isabellesym}
@@ -50,22 +49,19 @@
\begin{document}
-\renewcommand{\thefootnote}{$\star$}
-\footnotetext[1]{This paper is a revised, corrected and expanded version of \cite{ZhangUrbanWu12}.
+
+\title{Priority Inheritance Protocol Proved Correct$^\star$\thanks{$^\star$ This paper is a revised, corrected and expanded version of \cite{ZhangUrbanWu12}.
In Section 4 we improve our previous result by proving a finite bound for Priority Inversion.
Moreover, we are giving in this paper
more details about our proof and describe some of our (unverified) C-code for implementing the
Priority Inversion
Protocol, as well as surveying
the existing literature in more depth.
-Our C-code follows closely all results we proved about optimisations of the Priority Inheritance Protocol.
-}
-\renewcommand{\thefootnote}{\arabic{footnote}}
-
-\title{Priority Inheritance Protocol Proved Correct$^\star$}
-\author{Xingyuan Zhang$^1$, Christian Urban$^2$ and Chunhan Wu$^1$}
-\institute{PLA University of Science and Technology, China \and
- King's College London, United Kingdom}
+Our C-code follows closely all results we proved about optimisations of the Priority Inheritance Protocol.}}
+\titlerunning{Priority Inheritance Protocol Proved Correct}
+\author{Xingyuan Zhang \and Christian Urban \and Chunhan Wu}
+\institute{Chunhan Wu \and Xingyuan Zhang \at PLA University of Science and Technology Nanjing, China \and
+Christian Urban \at King's College London, United Kingdom}
\maketitle
\begin{abstract}
@@ -90,6 +86,7 @@
implementation builds on top of the small PINTOS operating system
used for teaching.\medskip
+\noindent
{\bf Keywords:} Priority Inheritance Protocol, formal correctness proof,
real-time systems, Isabelle/HOL
\end{abstract}