Formalna specifikacija sistema u TLA+

Šta je to formalna specifikacija?

Formalna specifikacija predstavlja matematički precizan opis ponašanja sistema kroz modele koji eliminišu nesigurnost i ambiguitet. Različiti sistemi, od hardvera do softvera, mogu se formalno specifikovati, pružajući inženjerima alate za jasno definisanje sistema. Motivacija za formalnu specifikaciju leži u eliminisanju nesporazuma u dizajnu i obezbeđivanju temeljne provere svojstava sistema.

Zašto nam je potrebna formalna specifikacija?

Formalna specifikacija ima široku primenu u raznim oblastima gde je ključno garantovati ispravnost, pouzdanost i performanse sistema. Evo nekoliko praktičnih primera kada je korisno koristiti formalnu specifikaciju:

Aero-svemirska Industrija: Avionski Kontrolni Sistemi - Garancija tačnosti i bezbednosti u upravljanju letom. Specifikacija sigurnosnih svojstava sistema i verifikacija da li se uvek održavaju u svim situacijama.
Telekomunikacije: Protokoli za Prenos Podataka gde formalnu specifikaciju možemo koristiti za obezbeđivanje da protokoli ispravno rade u svim uslovima, uključujući slučajeve gubitka podataka, zagušenja i otkaza čvorova.
Finansijski Sistemi: Transakcione Platforme - Garantovanje tačnosti i konzistentnosti transakcija, identifikacija i rešavanje problema vezanih za konkurenciju, osiguravanje očekivanog ponašanja u scenarijima sa greškama.
Bezbednost Računarskih Sistema: Kriptografski Protokoli - Garantovanje nepristrasnosti i sigurnosti kriptografskih protokola, identifikacija potencijalnih rizika i propusta u dizajnu pre implementacije.

Formalna specifikacija je posebno važna u kritičnim sistemima gde greške mogu imati ozbiljne posledice po bezbednost, zdravlje ili ekonomiju. Kroz ovu metodu, inženjeri mogu identifikovati, analizirati i rešavati probleme pre nego što sistemi postanu operativni, čime se smanjuje rizik od ozbiljnih neuspeha.

Kako bismo započeli celu diskusiju o TLA+, hajde prvo da vidimo kako bismo sistem mogli specifikovati formalno bez njega. Ako je sistem kontinuiran kao što su to mehanički sistemi ili dosta sistema u fizici, onda njega možemo specifikovati kroz diferencijalne jednačine. Kako se mi ovde mahom bavimo diskretnim sistemima, njihov ekvivalent bi bile diferencne jednačine. Problem sa ovim pristupom je što je broj mogućih stanja ogroman ili potencijalno beskonačan. Mi često želimo da proverimo da li su neka svojstva zadovoljena u svim stanjima ili u nekom podskupu mogućih stanja. Dobar model za predstavu sistema koji su diskretni i koji imaju lep način da se "prošetamo" kroz sve moguće konfiguracije tog sistema jesu zapravo mašine stanja.

Mašine stanja pružaju intuitivan način za modeliranje ponašanja sistema tokom vremena. Kroz precizno definisane tranzicije između stanja, možemo vizualizovati kako se sistem ponaša u različitim scenarijima.

TLA+ je formalni jezik za specifikaciju i verifikaciju sistema. Sintaksa TLA+ omogućava precizno izražavanje invarijanti sistema, što pomaže u garantovanju ispravnosti sistema tokom svih mogućih izvršenja.

Pogledajmo sledeći primer kako bismo se upoznali sa TLA+ sintaksom i semantikom i kako bismo uvideli na koji način TLA+ predstavlja mašine stanja.

------------------------ MODULE Primer ------------------------

VARIABLES state

Init == state = "Inicijalno" Next == state' = "Zavrseno" /\ state = "Inicijalno"

Spec == Init /\ [][Next]_state

==================================================================

U ovom primeru, Init inicijalizuje sistem, Next definiše tranzicije, a Spec koristi temporalnu logiku za proveru zadovoljivosti invarijante.

Ovde treba primetiti da smo u Next koristili zapravo dve promenljive, state i state'. Ovo je zapravo naša promenljiva state međutim u zavisnosti od toga da li koristimo state ili state' zavisi šta govorimo. Mi u TLA+ zapravo specifikujemo šta su sve validna stanja i šta su sve validne tranzicije pa tako Next opisuje sledeće: "Ako je state jednako Inicijalno, onda je jedino validno naredno stanje ono u kome je state jednako Zavrseno".

Na kraju, Spec je cela specifikacija koja kaže suštinski: "Validna stanja su takva da inicijalno važ Init a onda uvek važi Next".

Primer trivijalnog višenitnog programa

Razmotrimo jednostavan primer višenitnog programa u Javi koji predstavlja komunikaciju između dve niti.

public class KomunikacijaNiti { private static String poruka;

public static void main(String[] args) {
poruka = "";

Thread prvaNit = new Thread(() -> {
poruka = "Zdravo iz prve niti!";
});

Thread drugaNit = new Thread(() -> {
if (!poruka.isEmpty()) {
System.out.println("Poruka primljena: " + poruka);
}
});

prvaNit.start();
drugaNit.start();
}

}

Ovaj program definiše dve niti - prvaNit postavlja vrednost promenljive poruka, dok drugaNit proverava da li postoji poruka i ispisuje je ako postoji.

specifikacija ovakvog programa u TLA+ bi bila:

------------------------ MODULE VišenitniProgram ------------------------

VARIABLES poruka

Init == poruka = ""

PrvaNit == /\ poruka' = "Zdravo iz prve niti!" /\ UNCHANGED <>

DrugaNit == /\ poruka /= "" /\ Print("Poruka primljena: ", poruka) /\ UNCHANGED <>

Next == PrvaNit \/ DrugaNit

Spec == Init /\ [][Next]_<>

==================================================================

VARIABLES poruka: Deklaracija promenljive poruka koja se koristi za komunikaciju između niti.

Init: Početno stanje u kojem je poruka prazna.

PrvaNit: Akcija koju izvršava prva nit, postavljanje vrednosti poruka na "Zdravo iz prve niti!".

DrugaNit: Akcija koju izvršava druga nit, proverava da li postoji poruka i, ako postoji, ispisuje je.

Next: Definisanje tranzicija sistema kroz izvršavanje akcija PrvaNit i DrugaNit.

Spec: Specifikacija sistema koja garantuje da će se izvršavanje akcija očuvati tokom vremena.

Ova specifikacija precizno opisuje ponašanje višenitnog programa kroz formalni jezik TLA+.

TLA+ sintaksa

Deklaracija promenljivih (VARIABLES)

Deklaracija promenljivih definiše sve promenljive koje se koriste u specifikaciji. Na primer:

VARIABLES x, y, z

Ovde se deklarišu tri promenljive: x, y i z.

nicijalizacija sistema (Init)

Ova sekcija definiše početno stanje sistema. Na primer:

Init == x = 0 /\ y = 1 /\ z = 2 Ovde se postavlja početna vrednost promenljivih x, y i z.

Definisanje akcija (Next)

Akcije opisuju kako se sistem menja tokom vremena. Na primer:

Next == /\ x' = x + 1 /\ y' = y * 2 /\ z' = z - 1

Ovde se definišu tranzicije koje povećavaju vrednost x, dupliraju vrednost y i smanjuju vrednost z.

Invarijante (Spec)

Invarijante su tvrdnje koje treba da budu istinite tokom svih mogućih izvršenja sistema. Na primer:

Spec == x >= 0 /\ y > 0 /\ z <= 2

Ovde se definišu invarijante koje garantuju da vrednosti promenljivih ostaju unutar određenih granica.

Temporalna logika akcija ([], <>, =>, WF_, SF_)

Temporalna logika akcija se koristi za specifikaciju svojstava koja se odnose na tok izvršavanja akcija tokom vremena. Na primer:

Spec == Init /\ [][Next]_<<x, y, z>>

Ovde se koristi operator [ ] za označavanje da akcije opisane u Next sekciji moraju biti zadovoljene tokom svih mogućih izvršenja.

Operator <> se koristi za označavanje da će se svojstvo u nekom trenutku u budućnosti ostvariti. Na primer:

Spec == Init /\ <>(x > 10)

Die Hard problem - modelovanje i invarijanta

Problem sa deaktivacijom bombe iz filma "Umri muški" (Die Hard) uključuje korišćenje dve boce - jedne od 5 litara i druge od 3 litra - kako bi se dobilo tačno 4 litra vode, neophodno za deaktivaciju bombe. Scena je postala kultna zbog kombinacije napetosti i rešavanja problema u ograničenim uslovima.

Bombe su postavljene tako da se mogu deaktivirati samo ako se tačno 4 litra vode sipa u određeni spremnik.

Imamo dva spremnika, jedan od 5 litara i drugi od 3 litra, dostupni su za korišćenje.

Korišćenjem spremnika od 5 litara i 3 litra, napunite spremnik od 5 litara tačno sa 4 litra vode, kako biste deaktivirali bombu.

Hajde sada da ovu situaciju opišemo u TLA+. Ovde ćemo koristiti dve promenljive, jednu koja predstavlja količinu vode u spremniku od 5l i jednu koja predstavlja količinu vode u spremniku od 3l.

---- MODULE diehard ---- EXTENDS Integers, TLC VARIABLES big, small

typeOk == /\ small \in 0 .. 3 /\ big \in 0 .. 5

Init == small = 0 /\ big = 0

fillSmall == /\ small' = 3 /\ big' = big

fillBig == /\ small' = small /\ big' = 5

emptySmall == /\ small' = 0 /\ big' = big

emptyBig == /\ big' = 0 /\ small' = small smallToBig == IF small + big =< 5 THEN /\ big' = big + small /\ small' = 0 ELSE /\ big' = 5 /\ small' = small - 5 + big

bigToSmall == IF small + big =< 3 THEN /\ small' = big + small /\ big' = 0 ELSE /\ big' = big - 3 + small /\ small' = 3

Next == \/ fillSmall \/ fillBig
\/ emptySmall \/ emptyBig \/ smallToBig \/ bigToSmall

bigNotFour == big /= 4

Ovde imamo invarijantu bigNotFour koja kaže da spremnik od 5l ne sme da ima 4l vode. Kada pokrenemo validaciju ove specifikacije, TLA+ okruženje će nam reći kojim tranzicijama možemo doći do stanja koje ne zadovoljava ovo svojstvo odnosno do stanja kada u velikom spremniku imamo 4l vode.

PlusCal

PlusCal je jezik visokog nivoa koji olakšava pisanje TLA+ specifikacija. Evo primera:

------------------------ MODULE Heartbeat ------------------------

-- algorithm Heartbeat {

variables sender, receiver, heartbeat;

process Sender() {

while (TRUE) {

heartbeat := TRUE;

sender := !sender;

}

}

process Receiver() {

while (TRUE) {

receiver := !receiver;

if (heartbeat = FALSE) {

Error();

}

heartbeat := FALSE;

}

}

}

Ovde, koristimo PlusCal za modelovanje heartbeat protokola.

Zaključak

Formalna specifikacija, kroz alate kao što su TLA+ i PlusCal, pruža moćne mehanizme za dizajn, analizu i verifikaciju sistema. Kroz konkretne primere i kod, pokazali smo kako se ovi alati mogu koristiti za precizno opisivanje i garantovanje ispravnosti sistema. Njihova primena omogućava inženjerima da identifikuju i rešavaju potencijalne probleme na nivou dizajna, čime se povećava kvalitet i pouzdanost softvera.

Reference

YouTube kurs koji je napravio autor TLA+-a https://www.youtube.com/@tlavideocourse8540

Specifying systems knjiga https://lamport.azurewebsites.net/tla/book.html

PlusCal manual https://lamport.azurewebsites.net/tla/p-manual.pdf

Lainzine01