Comparing the QoS of Internet Audio Mechanisms via Formal Methods

We compute and compare the quality of service (QoS) of three soft real-time applications for audio transmission over the Internet. The main metric we want to capture is the average packet audio playout delay vs. the packet loss rate as perceived by users. Other metrics we take into account are the packet loss rate vs. the receiving buffer capacity, the lateness of discarded packets vs, average packet audio playout delay, and the waiting time in the receiver buffer for the played packets vs. the average packet audio playout delay. The study is conducted in the algebraic language EMPA, by way of formal descriptions of the three audio mechanisms. The mechanisms are analyzed via simulation using the software tool TwoTowers under various (experimentally obtained or randomly generated) traffic conditions. The stochastic process algebra EMPA is used because it compositionally supports system modeling, it allows functional properties of systems to be formally verified (unlike conventional simulators), and it represents generally distributed durations (which come into play in the three audio mechanisms). The comparison reveals that in general no one of the three mechanisms outperforms the other two, as their performance depends on the traffic conditions.