Promela

PROMELA ( Process or Protocol Meta Language ) är ett verifieringsmodelleringsspråk introducerat av Gerard J. Holzmann . Språket möjliggör dynamiskt skapande av samtidiga processer för att modellera, till exempel, distribuerade system . I PROMELA-modeller kan kommunikation via meddelandekanaler definieras som synkron (dvs. rendezvous) eller asynkron (dvs. buffrad). PROMELA-modeller kan analyseras med SPIN-modellkontrollen för att verifiera att det modellerade systemet producerar det önskade beteendet. En implementering verifierad med Isabelle/HOL finns också tillgänglig, som en del av projektet Computer Aided Verification of Automata (CAVA). Filer skrivna i Promela har traditionellt filändelsen .pml .

Introduktion

PROMELA är ett processmodelleringsspråk vars avsedda användning är att verifiera logiken i parallella system. Givet ett program i PROMELA Spin verifiera modellen för korrekthet genom att utföra slumpmässiga eller iterativa simuleringar av det modellerade systemets exekvering, eller så kan det generera ett C -program som utför en snabb uttömmande verifiering av systemtillståndsutrymmet. Under simuleringar och verifieringar kontrollerar SPIN frånvaron av blockerade låsningar, ospecificerade mottagningar och ej körbar kod. Verifieraren kan också användas för att bevisa riktigheten av systeminvarianter och den kan hitta exekveringscykler som inte fortskrider. Slutligen stöder den verifiering av linjära tidsmässiga begränsningar; antingen med Promela-anspråk eller genom att direkt formulera begränsningarna i tidslogiken . Varje modell kan verifieras med SPIN under olika typer av antaganden om miljön. När riktigheten av en modell har fastställts med SPIN, kan detta faktum användas vid konstruktion och verifiering av alla efterföljande modeller.

PROMELA-program består av processer, meddelandekanaler och variabler . Processer är globala objekt som representerar de samtidiga enheterna i det distribuerade systemet. Meddelandekanaler och variabler kan deklareras antingen globalt eller lokalt inom en process. Processer specificerar beteende, kanaler och globala variabler definierar miljön där processerna körs.

Språkreferens

Datatyper

De grundläggande datatyperna som används i PROMELA presenteras i tabellen nedan. Storlekarna i bitar anges för en PC i386/Linux-maskin.

namn	Storlek (bitar)	Användande	Räckvidd
bit	1	osignerad	0...1
bool	1	osignerad	0...1
byte	8	osignerad	0..255
mtype	8	osignerad	0..255
kort	16	signerad	−2 ¹⁵ ..2 ¹⁵ − 1
int	32	signerad	−2 ³¹ ..2 ³¹ − 1

Namnen bit och bool är synonymer för en enskild informationsbit. En byte är en kvantitet utan tecken som kan lagra ett värde mellan 0 och 255. korta s och int s är tecken med tecken som endast skiljer sig i det värdeintervall de kan innehålla.

Variabler kan också deklareras som matriser. Till exempel, deklarationen:

    int  x  [  10  ];

deklarerar en matris med 10 heltal som kan nås i matrisnedsänkta uttryck som:

x[0] = x[1] + x[2];

Men arrayerna kan inte räknas upp när de skapas, så de måste initieras enligt följande:

  
 0  
   
    int  x  [  3  ];  x  [  ]  =  1  ;  x  [  1  ]  =  2  ;  x  [  2  ]  =  3  ;

Indexet till en array kan vara vilket uttryck som helst som bestämmer ett unikt heltalsvärde. Effekten av ett index utanför intervallet är odefinierad. Flerdimensionella arrayer kan definieras indirekt med hjälp av typedef -konstruktionen (se nedan).

Processer

Tillståndet för en variabel eller en meddelandekanal kan endast ändras eller inspekteras av processer. En processs beteende definieras av en proctype -deklaration. Till exempel deklarerar följande en processtyp A med ett variabeltillstånd:

proctype A() { byte state; tillstånd = 3; }

Proctype - definitionen deklarerar bara processbeteende, den exekverar det inte. Till en början, i PROMELA-modellen, kommer bara en process att exekveras: en process av typen init , som måste deklareras uttryckligen i varje PROMELA-specifikation.

Nya processer kan skapas med hjälp av run -satsen, som tar ett argument som består av namnet på en proctype , från vilken en process sedan instansieras. Köroperatorn kan användas i huvuddelen av proctypedefinitionerna , inte bara i den initiala processen . Detta möjliggör dynamiskt skapande av processer i PROMELA.

En exekveringsprocess försvinner när den avslutas – det vill säga när den når slutet av texten i proctypedefinitionen, och alla underordnade processer som den startade har avslutats.

En proctype kan också vara aktiv (nedan).

Atomkonstruktion

Genom att prefixet en sekvens av uttalanden inneslutna i klammerparenteser med nyckelordet atomic , kan användaren indikera att sekvensen ska exekveras som en odelbar enhet, icke-interfolierad med andra processer.

atomic { uttalanden; }

Atomsekvenser kan vara ett viktigt verktyg för att minska komplexiteten hos verifieringsmodeller. Observera att atomsekvenser begränsar mängden interfoliering som är tillåten i ett distribuerat system. Intraktabla modeller kan göras handhavbara genom att märka alla manipulationer av lokala variabler med atomsekvenser.

Meddelandet passerar

Meddelandekanaler används för att modellera överföringen av data från en process till en annan. De deklareras antingen lokalt eller globalt, till exempel enligt följande:

chan qname = [16] av {kort}

Detta förklarar en buffrad kanal som kan lagra upp till 16 meddelanden av typen kort ( kapaciteten är 16 här).

Påståendet:

qnamn! expr;

skickar värdet av uttrycket expr till kanalen med namnet qname , det vill säga det lägger till värdet till kanalens svans.

Påståendet:

qnamn? meddelande;

tar emot meddelandet, hämtar det från kanalens huvud och lagrar det i variabeln msg. Kanalerna skickar meddelanden i först-in-först-ut-ordning.

En rendezvous-port kan deklareras som en meddelandekanal med butikslängden noll. Till exempel följande:

chan port = [0] av {byte}

definierar en rendezvous-port som kan skicka meddelanden av typen byte . Meddelandeinteraktioner via sådana rendezvous-portar är per definition synkrona, dvs. avsändare eller mottagare (den som anländer först till kanalen) kommer att blockera för den utmanare som anländer som andra (mottagare eller sändare).

När en buffrad kanal har fyllts till sin kapacitet (sändning är "kapacitet" antal utgångar före mottagning av ingångar), är standardbeteendet för kanalen att bli synkront, och avsändaren kommer att blockera vid nästa sändning. Observera att det inte finns någon gemensam meddelandebuffert som delas mellan kanaler. Ökande komplexitet, jämfört med att använda en kanal som enkelriktad och punkt till punkt, är det möjligt att dela kanaler mellan flera mottagare eller flera sändare, och att slå samman oberoende dataströmmar till en enda delad kanal. Av detta följer att en enda kanal också kan användas för dubbelriktad kommunikation.

Kontrollflödeskonstruktioner

Det finns tre kontrollflödeskonstruktioner i PROMELA. De är fallvalet , upprepningen och det ovillkorliga hoppet .

Val av fall

Den enklaste konstruktionen är urvalsstrukturen. Med hjälp av de relativa värdena för två variabler a och b , till exempel, kan man skriva:

om :: (a != b) -> alternativ1 :: (a == b) -> alternativ2 fi

Urvalsstrukturen innehåller två exekveringssekvenser, var och en föregås av ett dubbelt kolon. En sekvens från listan kommer att exekveras. En sekvens kan endast väljas om dess första sats är körbar. Den första satsen i en kontrollsekvens kallas en guard .

I exemplet ovan utesluter vakterna varandra, men de behöver inte vara det. Om mer än en vakt är körbar, väljs en av motsvarande sekvenser icke-deterministiskt. Om alla vakter inte kan köras kommer processen att blockeras tills en av dem kan väljas. (Tvärtom skulle occam - programmeringsspråket sluta eller inte kunna fortsätta utan körbara skydd.)

om :: (A == sant) -> alternativ1; :: (B == sant) -> alternativ2; /* Kan komma hit även om A==true */ :: else -> fallthrough_option; fi

Konsekvensen av det icke-deterministiska valet är att i exemplet ovan, om A är sant, kan båda valen tas . I "traditionell" programmering skulle man förstå en om – om – annat struktur sekventiellt. Här om – dubbla kolon – dubbla kolon förstås som "alla som är redo" och om ingen är redo, först då skulle den andra tas.

om :: värde = 3; :: värde = 4; fi

I exemplet ovan ges värdet icke-deterministiskt värdet 3 eller 4.

Det finns två pseudo-satser som kan användas som skydd: timeout -satsen och else- satsen. Timeout - satsen modellerar ett speciellt tillstånd som tillåter en process att avbryta väntan på ett tillstånd som kanske aldrig blir sant. else-satsen kan användas som den initiala satsen för den sista alternativsekvensen i en urvals- eller iterationssats. Det andra är bara körbart om alla andra alternativ i samma urval inte är körbara. Dessutom får den andra inte användas tillsammans med kanaler.

Upprepning (loop)

En logisk förlängning av urvalsstrukturen är upprepningsstrukturen. Till exempel:

gör :: count = count + 1 :: a = b + 2 :: (count == 0) -> break od

beskriver en upprepningsstruktur i PROMELA. Endast ett alternativ kan väljas åt gången. När alternativet är klart upprepas exekveringen av strukturen. Det normala sättet att avsluta upprepningsstrukturen är med en break- sats. Den överför kontrollen till instruktionen som omedelbart följer upprepningsstrukturen.

Ovillkorliga hopp

Ett annat sätt att bryta en loop är goto -satsen. Till exempel kan man ändra exemplet ovan enligt följande:

do :: count = count + 1 :: a = b + 2 :: (count == 0) -> goto done od done: hoppa över;

Goto i detta exempel hoppar till en etikett som heter done . En etikett kan bara visas före ett uttalande. För att hoppa i slutet av programmet, till exempel, är en dummy-sats skip användbar: det är en platshållare som alltid är körbar och har ingen effekt.

Påståenden

En viktig språkkonstruktion i PROMELA som behöver lite förklaring är påstående uttalandet. Uttalanden av formuläret:

hävda(any_boolean_condition)

är alltid körbara. Om ett angivet booleskt villkor gäller, har uttalandet ingen effekt. Om emellertid villkoret inte nödvändigtvis håller, kommer uttalandet att ge ett fel under verifieringar med SPIN .

Komplexa datastrukturer

En PROMELA typedef- definition kan användas för att introducera ett nytt namn för en lista över dataobjekt av fördefinierade eller tidigare definierade typer. Det nya typnamnet kan användas för att deklarera och instansiera nya dataobjekt, som kan användas i alla sammanhang på ett uppenbart sätt:

  
 
      
      
  typedef  MyStruct  {  short  Field1  ;  byte  Fält2  ;  };

Åtkomsten till fälten som deklareras i en typedef- konstruktion görs på samma sätt som i programmeringsspråket C. Till exempel:

MyStruct x; x.Fält1 = 1;

är en giltig PROMELA-sekvens som tilldelar fältet Fält1 för variabeln x värdet 1 .

Aktiva proctyper

Det aktiva nyckelordet kan ha prefix till valfri proctypedefinition . Om nyckelordet finns kommer en instans av den proctypen att vara aktiv i det initiala systemtillståndet. Flera instansieringar av den proctypen kan specificeras med ett valfritt arraysuffix av nyckelordet. Exempel:

aktiv proctype A() { ... } aktiv [4] proctype B() { ... }

Körbarhet

Semantiken för körbarhet tillhandahåller de grundläggande medlen i Promela för modellering av processsynkroniseringar.

mtype = {M_UP, M_DW}; chan Chan_data_down = [0] av {mtype}; chan Chan_data_up = [0] av {mtype}; proctype P1 (chan Chan_data_in, Chan_data_out) { do :: Chan_data_in ? M_UP -> hoppa över; :: Chan_data_out ! M_DW -> hoppa över; od; }; proctype P2 (chan Chan_data_in, Chan_data_out) { do :: Chan_data_in ? M_DW -> hoppa över; :: Chan_data_out ! M_UP -> hoppa över; od; }; init { atomic { kör P1 (Chan_data_up, Chan_data_down); kör P2 (Chan_data_down, Chan_data_up); } }

I exemplet har de två processerna Pl och P2 icke-deterministiska val av (1) input från den andra eller (2) utmatning till den andra. Två rendezvous-handslag är möjliga, eller körbara , och en av dem är vald. Detta upprepas för alltid. Därför kommer denna modell inte att låsa fast.

När Spin analyserar en modell som ovan, kommer den att verifiera valen med en icke-deterministisk algoritm, där alla körbara val kommer att utforskas. Men när Spins simulator visualiserar möjliga icke-verifierade kommunikationsmönster, kan den använda en slumpgenerator för att lösa det "icke-deterministiska" valet. Därför kan simulatorn misslyckas med att visa ett dåligt utförande (i exemplet finns det inget dåligt spår). Detta illustrerar skillnaden mellan verifiering och simulering. Dessutom är det också möjligt att generera körbar kod från Promela-modeller med hjälp av Refinement.

Nyckelord

Följande identifierare är reserverade för användning som nyckelord.

aktiva
hävda
atom-
bit
bool
ha sönder
byte
chan
d_step
D_proctype
do
annan
tömma
aktiverad
fi
full
gå till
dold
om
i kö
i det
int
len
mtype
tömma
aldrig
nfull
od
av
pc_värde
printf
prioritet
prototyp
försedd
springa
kort
hoppa
Paus
typdef
såvida inte
osignerad
xr
xs

externa länkar