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 consider to capture the user perception of audio is the average packet audio playout delay vs. the packet loss rate. Other metrics we take into account are the packet loss rate vs. the receiving buffer capacity, the lateness of discarded packets vs. the 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 on formal descriptions of the three audio mechanisms expressed in the process algebraic language EMPA, which are analyzed via simulation through the software tool TwoTowers under various (experimentally obtained or randomly generated) traffic conditions. The stochastic process algebra EMPA has been used because of its compositional support to system modeling, its adequacy to allow functional properties of systems to be formally verified (unlike conventional simulators), and its capability of representing generally distributed durations (which come into play in the three audio mechanisms). The comparison reveals that neither of the three mechanisms outperforms the other two in general, as their performance depends on the traffic conditions.