Dans le système {se Orccad} les lois de commande temps-réel et multicadence sont implantées sous la forme d’un réseau de tâches communicantes plus ou moins fortement synchronisées, sous le contrôle d’un système d’exploitation temps-réel. Des simulations et des expériences sur site réel ont montré qu’une synchronisation partielle judicieuse de ces tâches permet d’améliorer l’efficacité de ces lois de commande. Nous montrons que l’introduction de synchronisations peut cependant introduire des problèmes de type interblocages ou incohérences de spécification. Une modélisation à l’aide de réseaux de Petri permet de vérifier formellement l’absence d’interblocage dans le réseau de tâches synchronisées et de détecter l’absence d’un certain type d’incohérence temporelle. Finalement, des conditions suffisantes permettant de construire ces lois de commande efficaces et exemptes d’interblocages sont données.