Use of Timed Automata Models in the Design of Real-time Control Network Elements

The design of network elements for real-time control networks requires careful consideration of the fundamental timing requirements. The use of a timed automata approach for modelling and verifying the timing requirements promises to be beneficial. In this work a case study approach is shown where a model of the packet scheduler component for a network switch element is developed, based on a timed automata method. Using the Uppaal model checker certain properties are verified. The timed behaviour of the model can be assessed, based on clocks incorporated into the timed automata model.