\documentclass[runningheads]{llncs}+
−
\usepackage{isabelle}+
−
\usepackage{isabellesym}+
−
\usepackage{amsmath}+
−
\usepackage{amssymb}+
−
%\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}+
−
+
−
\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{$\_\!\_$}}+
−
+
−
\newcommand{\isasymcalL}{\ensuremath{\cal{L}}}+
−
\newcommand{\isasymbigplus}{\ensuremath{\bigplus}}+
−
+
−
\newcommand{\bigplus}{\mbox{\Large\bf$+$}}+
−
\begin{document}+
−
+
−
\title{A Formalisation of Priority Inheritance Protocol \\ +
−
       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, United Kingdom}+
−
\maketitle+
−
+
−
\begin{abstract}+
−
In realtime systems with support for resource locking and for+
−
processes with 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 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 the+
−
original proof by making all notions precise and implementing 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}+
−
+
−
\bibliographystyle{plain}+
−
\bibliography{root}+
−
+
−
\end{document}+
−
+
−
%%% Local Variables:+
−
%%% mode: latex+
−
%%% TeX-master: t+
−
%%% End:+
−