1 \documentclass[runningheads]{llncs}

     2 \usepackage{isabelle}

     3 \usepackage{isabellesym}

     4 \usepackage{amsmath}

     5 \usepackage{amssymb}

     6 \usepackage{tikz}

     7 \usepackage{pgf}

     8 %\usetikzlibrary{arrows,automata,decorations,fit,calc}

     9 %\usetikzlibrary{shapes,shapes.arrows,snakes,positioning}

    10 %\usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf

    11 %\usetikzlibrary{matrix}

    12 \usepackage{pdfsetup}

    13 \usepackage{ot1patch}

    14 \usepackage{times}

    15 %%\usepackage{proof}

    16 %%\usepackage{mathabx}

    17 \usepackage{stmaryrd}

    18 \usepackage{url}

    19 

    20 \titlerunning{Myhill-Nerode using Regular Expressions}

    21 

    22 

    23 \urlstyle{rm}

    24 \isabellestyle{it}

    25 \renewcommand{\isastyleminor}{\it}%

    26 \renewcommand{\isastyle}{\normalsize\it}%

    27 

    28 

    29 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}

    30 \renewcommand{\isasymequiv}{$\dn$}

    31 \renewcommand{\isasymemptyset}{$\varnothing$}

    32 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}

    33 

    34 \newcommand{\isasymcalL}{\ensuremath{\cal{L}}}

    35 \newcommand{\isasymbigplus}{\ensuremath{\bigplus}}

    36 

    37 \newcommand{\bigplus}{\mbox{\Large\bf$+$}}

    38 \begin{document}

    39 

    40 \title{A Formalisation of Priority Inheritance Protocol \\ 

    41        for Correct and Efficient Implementation}

    42 \author{Xingyuan Zhang\inst{1} \and Christian Urban\inst{2} \and Chunhan Wu\inst{1}}

    43 \institute{PLA University of Science and Technology, China \and 

    44            King's College, University of London, U.K.}

    45 \maketitle

    46 

    47 %\mbox{}\\[-10mm]

    48 \begin{abstract}

    49 Despite the wide use of Priority Inheritance Protocol in real time operating

    50 system, it's correctness has never been formally proved and mechanically checked. 

    51 All existing verification are based on model checking technology. Full automatic

    52 verification gives little help to understand why the protocol is correct. 

    53 And results such obtained only apply to models of limited size. 

    54 This paper presents a formal verification based on theorem proving. 

    55 Machine checked formal proof does help to get deeper understanding. We found 

    56 the fact which is not mentioned in the literature, that the choice of next 

    57 thread to take over when an critical resource is release does not affect the correctness

    58 of the protocol. The paper also shows how formal proof can help to construct 

    59 correct and efficient implementation. 

    60 \end{abstract}

    61 

    62 

    63 \input{session}

    64 

    65 %%\mbox{}\\[-10mm]

    66 \bibliographystyle{plain}

    67 \bibliography{root}

    68 

    69 \end{document}

    70 

    71 %%% Local Variables:

    72 %%% mode: latex

    73 %%% TeX-master: t

    74 %%% End: