Promela ( PROTOKOLL Metasprache ) ist eine Spezifikationssprache für asynchrone Systeme, die in anderen Worten bedeutet , dass diese Sprache die Beschreibung der gleichzeitigen Systeme, wie beispiels ermöglicht Protokolle die Kommunikation . Es ermöglicht die dynamische Erstellung von Prozessen. Die Kommunikation zwischen diesen verschiedenen Prozessen kann durch gemeinsame Nutzung globaler Variablen oder über Kommunikationskanäle erfolgen. Es ist somit möglich, synchrone oder asynchrone Kommunikation zu simulieren.
In PROMELA gibt es keinen Unterschied zwischen Anweisungen und Bedingungen. Eine Anweisung kann nur übergeben werden, wenn sie ausführbar ist, eine Bedingung nur, wenn sie wahr ist. Andernfalls wird der Prozess blockiert, bis die Bedingung erfüllt ist.
Promela ist mit dem Spin-Validierungs-Tool verknüpft.