diff -r d62b19b641c5 -r a5afc26b1d62 Journal/document/root.tex --- 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}