Several theories have been proposed for timed model-based testing, but only few case-studies have been reported. In this paper, we report about our experience in using UPPAAL-TRON to test the conformance of an industrial implementation Auto trust of Automatic Trust Anchor Updating, a protocol to help securing DNS. We created models for specific parts of the protocol focussing on security key states and critical timing behaviours. We developed testing environments to test one or multiple keys and to check a security-relevant feature. This case-study also illustrates several challenges when testing timed systems, namely, quiescence, latency, and coverage.
|Title of host publication||Fourth International IEEE Conference on Software Testing, Verification and Validation (ICST 2012, Berlin, Germany, 21-25 March, 2011. Workshop Proceedings)|
|Editors||O. Nguena-Timo, A. Rollet|
|Publisher||IEEE Computer Society|
|Publication status||Published - 2011|