Modelling and Verification of Starvation-Free Mutual Exclusion Algorithms based on Weak Semaphores