We show how HyTech, a symbolic model checker for linear hybrid systems, can be used to analyze an audio control protocol. The protocol was first verified by Bosscher et al. without computer support. They provided necessary and sufficient conditions for its correctness. In this paper, we demonstrate that algorithmic methods can not only verify the protocol, but can also automatically synthesize the bound on the maximum admissible clock drift, and suggest design modifications for a more robust protocol.
In the course of this case study, we show how to overcome various apparent obstacles to the use of algorithmic analysis methods. We believe the techniques we use provide insight to the practictioner interested in modeling and analyzing similar real-world applications. Firstly, symbolic model-checking is expressive: it is not limited to systems with discrete state spaces, but indeed HyTech is able to verify infinite state systems with continuous variables subject to variable rates of change. Secondly, we show that the transmission of arbitrary length messages can be modeled using only finite-state data information. Thirdly, timing properties involving arbitrarily large timing constants are also verified. Fourthly, model checking can give useful insight into a system. HyTech is able to infer automatically the maximum tolerable clock error and suggests where the error bound is tight. The tool can then verify that a revised protocol has a wider error tolerance.
Proceedings of the Seventh International Conference on Computer-aided Verification (CAV 1995), Lecture Notes in Computer Science 939, Springer-Verlag, 1995, pp. 381-394.