Formal specifications and proofs of inheritance protocols for real-time scheduling

Priority is one means of representing scheduling information in a concurrent real-time programming language. Unfortunately, a static priority scheme can give rise to inversion when combined with synchronisation primitives. The use of semaphores for protecting access to critical regions is investigated using the formal notation Z. It is shown that the normal semantics for semaphores can lead to a high priority process being delayed indefinitely. The inclusion of inheritance into the semaphore model improves the situation, but delays can still be significant. To overcome this lack of responsiveness, Lui Sha et al., (1987), have developed a ceiling protocol that both removes the possibility of deadlock and limits (to one) the number of times a high priority process can be blocked. A formal specification of a complete and a simplified version of the ceiling protocol, together with proofs of their important properties are presented