Avtomatska tvorba modelov s sondami iz specifikacije sistema v jeziku SDL

Dodeljena: 1. 10. 1999
Zagovarjana: 8. 9. 2004
Študent: Boštjan Vlaovič

Povzetek naloge:

Doktorska disertacija predstavlja rezultate raziskav avtomatske tvorbe modelov v jeziku Promela iz specifikacije sistema v jeziku SDL. V splošnem se model sistema lahko pridobi ročno ali avtomatsko. Model sistema lahko ob ročnem pristopu tvori le strokovnjak z dobrim poznavanjem delovanja sistema in jezika za opis modelov. Kvaliteta modela je neposredno odvisna od strokovnjaka. Pri postopku ročne gradnje modela hitro pride do napak pri modeliranju lastnosti sistema. Disertacija formalno podaja algoritme za avtomatsko tvorbo modelov v jeziku Promela.

Tehnika preverjanja modelov nam lahko z matematično natančnostjo potrdi ali ovrže skladnost podanega modela sistema s specifikacijo zahtev. Za preverjanje lastnosti je potrebno v model sistema namestiti sonde. Te nam omogočajo opazovanje sprememb v modelu. Disertacija definira postopke za avtomatsko dopolnitev modela s sondami.

Teoretične raziskave smo podkrepili s praktično realizacijo algoritmov v orodju sdl2pml. Z njim smo uspešno verificirali specifikacijo protokola V.76. Vsi uporabljeni modeli protokola V.76 v disertaciji so pridobljeni avtomatično. Pregled doseženih rezultatov pokaže obetavnost pristopa in njegovo praktično vrednost.