Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol