L'utilisation dans le cadre des réseaux sans fil de multiples canaux orthogonaux au niveau des protocoles MAC offre une grande potentialité pour améliorer, par rapport à la communication mono-canal, le débit des transmissions. Toutefois, le contexte multi-canal nécessite une fonction supplémentaire au niveau MAC qui porte sur l'allocation et la coordination des canaux. Plusieurs variantes d'allocation de canaux ont été définies et proposées dans la littérature. Cependant, il existe peu d'études basées sur des techniques formelles afin de vérifier les propriétés fondamentales des mécanismes d'allocation. Le but de cet article est précisément de proposer une modélisation formelle et la vérification des protocoles MAC multi-canaux basés sur l'approche du canal dédié à l'aide du modèle RdPTS (Réseaux de Petri Temporisés Stochastiques). Nous vérifions la propriété de réservation en termes d'utilisation en exclusion mutuelle des canaux de données.