Automated analysis of an audio control protocol

Abstract

We show how HyTech, a symbolic model checker for linear hybrid systems, can be used to analyze an audio control protocol. This protocol [BPV94] was first verified by Bosscher et al. without computer support. In this paper, we demonstrate that algorithmic methods can not only verify the protocol, but can also automatically synthesize the bound on the maximum clock drift, and suggest design modification for a more robust protocol. We believe the techniques we used — finite state encodings, automata transformations, strengthening of specifications — provide insight to the practictioner interested in modeling and analyzing similar real-world applications.