La composition de services est une tâche primordiale dans le développement de systèmes orientés service. L'orchestration se présente comme un ensemble de mécanismes pour la composition d'un nouveau service web formé d'un ensemble de services atteignables. Afin de valider une telle composition, deux classes de propriétés non fonctionnelles doivent être prises en considération à savoir les propriétés génériques et les propriétés spécifiques. Les propriétés génériques peuvent être vérifiées pour tous les services web invoqués dans une orchestration. Les propriétés spécifiques constituent les relations d'interdépendance entre les différentes activités au sein d'un processus d'orchestration. Ces propriétés ne peuvent pas être vérifiées directement sur le processus, l'utilisation donc d'une technique formelle s'avère intéressante. Pour se faire, nous présenterons dans cet article notre approche formelle pour la validation d'une orchestration de services web. L'approche adopte BPEL 2.0 (Business Process Execution Language) comme langage d'orchestration de services web et utilise le model-checker SPIN pour la vérification. La spécification BPEL est traduite en code Promela, le langage de spécification de SPIN, afin de vérifier aussi bien les propriétés génériques que les propriétés spécifiques exprimées en LTL (Linear Temporal Logic). L'outil de transformation de BPEL en Promela est développé en utilisant ANTLR (ANother Tool for Language Recognition). Ce travail a été couronné par le développement de l'outil {\sc BpelVT} (BPEL Verification Tool) afin de consolider l'approche proposée.
