PROMELA
PROMELA (PROtocol MEta LAnguage) est un langage de spécification de systèmes asynchrones, ce qui en d'autres termes veut dire que ce langage permet la description de systèmes concurrents, comme les protocoles de communication. Il autorise la création dynamique de processus. La communication entre ces différents processus peut se faire en partageant les variables globales ou alors en utilisant des canaux de communication. On peut ainsi simuler des communications synchrones ou asynchrones.
En PROMELA, il n'y a pas de différence entre les instructions et les conditions. Une instruction ne peut être passée que si elle est exécutable, une condition que si elle est vraie. Sinon le processus est bloqué jusqu'à ce que la condition devienne vraie.
Promela est associé à l'outil de validation Spin.