Les automatismes industriels et domestiques sont fréquemment mis en oeuvre au moyen de contrôleurs logiques programmables (CLP), qui exécutent en mode synchrone des applications embarquées interagissant avec leur environnement. En combinant plusieurs CLP qui opèrent indépendamment et communiquent à travers un réseau, il est possible de réaliser des automatismes plus élaborés, de type GALS (Globally Asynchronous, Locally Synchronous). Pour assurer une conception correcte des systèmes GALS, qui est difficile à cause de la présence simultanée des aspects synchrones et asynchrones, nous proposons dans cet article une méthodologie rigoureuse, basée sur des méthodes formelles et des techniques de validation automatique (test et vérification) issues des paradigmes synchrone et asynchrone.