Carsten Rütz.

Bachelor thesis in .pdf here.

Supporting Materials

.zip archive here

Abstract

We investigate the usability of Timed Model-Based Testing in a case study: Conformance of the implementation Autotrust with Automatic Trust Anchor Updating, a protocol to help securing DNS. We present models for timing aspects of the protocol. Definition of checks on quiescence in the model are proven to be possible. Latency during input application can yield false test results. We present a model to validate a security-relevant missing feature of Autotrust. Reuse of an existing model of the protocol, designed for model-checking, is shown to be infeasible. Finally, we show that the implementation Autotrust behaves according to the tested part of its specification.