A Simulative Analysis of Internet Audio Mechanisms Using Formal Methods