equal
deleted
inserted
replaced
43 King's College London, United Kingdom} |
43 King's College London, United Kingdom} |
44 \maketitle |
44 \maketitle |
45 |
45 |
46 \begin{abstract} |
46 \begin{abstract} |
47 In real-time systems with support for resource locking and for |
47 In real-time systems with support for resource locking and for |
48 processes with priorities, one faces the problem of priority |
48 processes with priorities, one faces the problem of Priority |
49 inversion. This problem can make the behaviour of processes |
49 IBnversion. This problem can make the behaviour of processes |
50 unpredictable and the resulting bugs can be hard to find. The |
50 unpredictable and the resulting bugs can be hard to find. The |
51 Priority Inheritance Protocol is one solution implemented in many |
51 Priority Inheritance Protocol is one solution implemented in many |
52 systems for solving this problem, but the correctness of this solution |
52 systems for solving this problem, but the correctness of this solution |
53 has never been formally verified in a theorem prover. As already |
53 has never been formally verified in a theorem prover. As already |
54 pointed out in the literature, the original informal investigation of |
54 pointed out in the literature, the original informal investigation of |