In this paper, we study the formal modelling and verification of a
network player system using Duration Calculus, a real time interval
temporal logic. The system is modelled by the conjunction of a number
of Duration Calculus formulae each capturing a basic property of the
system. That the system satisfies the requirement is expressed by the
entailment of the requirement formula from the system formula. We use
an automated tool DCValid for verification. DCValid is a model
checking tool and it cannot verify our system in the general form, and
therefore a special instance is derived from the general model and
subsequently checked using DCValid.