equal
deleted
inserted
replaced
60 uncovers facts not mentioned in the literature, but also shows how to |
60 uncovers facts not mentioned in the literature, but also shows how to |
61 efficiently implement this protocol. Earlier correct implementations |
61 efficiently implement this protocol. Earlier correct implementations |
62 were criticised as too inefficient. Our formalisation is based on |
62 were criticised as too inefficient. Our formalisation is based on |
63 Paulson's inductive approach to verifying protocols.\medskip |
63 Paulson's inductive approach to verifying protocols.\medskip |
64 |
64 |
65 {\bf Keywords:} Priority Inheritance Protocol, formal connectness proof, |
65 {\bf Keywords:} Priority Inheritance Protocol, formal correctness proof, |
66 real-time systems, Isabelle/HOL |
66 real-time systems, Isabelle/HOL |
67 \end{abstract} |
67 \end{abstract} |
68 |
68 |
69 \input{session} |
69 \input{session} |
70 |
70 |