1 \documentclass[runningheads]{llncs} |
1 \documentclass[runningheads]{llncs} |
2 \usepackage{isabelle} |
2 \usepackage{isabelle} |
3 \usepackage{isabellesym} |
3 \usepackage{isabellesym} |
4 \usepackage{amsmath} |
4 \usepackage{amsmath} |
5 \usepackage{amssymb} |
5 \usepackage{amssymb} |
6 \usepackage{tikz} |
6 %\usepackage{tikz} |
7 \usepackage{pgf} |
7 %\usepackage{pgf} |
8 %\usetikzlibrary{arrows,automata,decorations,fit,calc} |
8 %\usetikzlibrary{arrows,automata,decorations,fit,calc} |
9 %\usetikzlibrary{shapes,shapes.arrows,snakes,positioning} |
9 %\usetikzlibrary{shapes,shapes.arrows,snakes,positioning} |
10 %\usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf |
10 %\usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf |
11 %\usetikzlibrary{matrix} |
11 %\usetikzlibrary{matrix} |
12 \usepackage{pdfsetup} |
12 \usepackage{pdfsetup} |
43 \institute{PLA University of Science and Technology, China \and |
43 \institute{PLA University of Science and Technology, China \and |
44 King's College London, United Kingdom} |
44 King's College London, United Kingdom} |
45 \maketitle |
45 \maketitle |
46 |
46 |
47 \begin{abstract} |
47 \begin{abstract} |
48 In realtime systems with support for resource locking and processes |
48 In realtime systems with support for resource locking and for |
49 involving priorities, one faces the problem of priority |
49 processes with priorities, one faces the problem of priority |
50 inversion. This problem can make the behaviour of processes |
50 inversion. This problem can make the behaviour of processes |
51 unpredictable and the resulting bugs can be hard to find. The |
51 unpredictable and the resulting bugs can be hard to find. The |
52 Priority Inheritance Protocol is one solution implemented in many |
52 Priority Inheritance Protocol is one solution implemented in many |
53 systems for solving this problem, but the correctness of this solution |
53 systems for solving this problem, but the correctness of this solution |
54 has never been formally verified in a theorem prover. As already |
54 has never been formally verified in a theorem prover. As already |
55 pointed out in the literature, the original description of the |
55 pointed out in the literature, the original informal investigation of |
56 Property Inheritance Protocol presents an informal correctness |
56 the Property Inheritance Protocol presents a correctness ``proof'' for |
57 ``proof'' for an \emph{incorrect} algorithm. In this paper we fix the |
57 an \emph{incorrect} algorithm. In this paper we fix the problem of the |
58 problem of the original proof by making all notions precise and |
58 original proof by making all notions precise and implementing a |
59 implementing a variant of a solution proposed earlier. Our |
59 variant of a solution proposed earlier. Our formalisation in |
60 formalisation in Isabelle/HOL uncovered facts not mentioned in the |
60 Isabelle/HOL uncovered facts not mentioned in the literature, but also |
61 literature, but also shows how to efficiently implement this |
61 shows how to efficiently implement this protocol. Earlier correct |
62 protocol. Earlier correct implementations were criticised as too |
62 implementations were criticised as too inefficient. Our formalisation |
63 inefficient. Our formalisation is based on Paulson's inductive |
63 is based on Paulson's inductive approach to verifying |
64 approach to verifying protocols.\medskip |
64 protocols.\medskip |
65 |
65 |
66 {\bf Keywords:} Priority Inheritance Protocol, formal connectness proof, |
66 {\bf Keywords:} Priority Inheritance Protocol, formal connectness proof, |
67 realtime systems |
67 realtime systems |
68 \end{abstract} |
68 \end{abstract} |
69 |
69 |