Promela

Promela (proces sau protocol meta -limbaj) este un limbaj de modelare de verificare introdus de Gerard J.

Holzmann.

Limbajul permite crearea dinamică a proceselor concomitente pentru a modela, de exemplu, sisteme distribuite.

În modelele Promela, comunicarea prin canale de mesaje poate fi definită ca fiind sincronă (adică, Rendezvous) sau asincronă (adică, tamponată).

Modelele Promela pot fi analizate cu verificatorul modelului de spin, pentru a verifica dacă sistemul modelat produce comportamentul dorit.

De asemenea, este disponibilă o implementare verificată cu Isabelle/HOL, ca parte a proiectului de verificare a computerului automat (CAVA).

Fișierele scrise în Promela au în mod tradițional o extensie de fișiere .PML.