An Experience Report on an Industrial CaseStudy about Timed Model-Based Testing with UPPAAL-TRON
Several theories have been proposed for timed model-based testing, but only few case-studies have been re- ported. In this paper, we report about our experience in using UPPAAL-TRON to test the conformance of an industrial imple- mentation AUTOTRUST 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.