Verification of a fieldbus scheduling protocol using timed automata

This paper deals with the formal verification of a fieldbus real-time scheduling mechanism, using the notion of timed-automata and the UPPAAL model checker. A new approach is proposed here that treats the set of schedulers that regulate access on a fieldbus as a separate entity, called the scheduling layer. In addition a network with a changing topology is considered, where nodes may be turned on or off. The behaviour of the scheduling layer in conjunction with the data link, the medium and the network management layer is examined and it is proved that it enjoys a number of desirable properties