• Znanost
  • Razširitev avtomatskega modeliranja SDL specifikacij v Promeli z vključevanjem gradnikov v jeziku C in novim modelom diskretnega časa
 
29. 3. 2006

Razširitev avtomatskega modeliranja SDL specifikacij v Promeli z vključevanjem gradnikov v jeziku C in novim modelom diskretnega časa

Dodeljena: 1. 10. 2001 
Zagovarjana: 29. 3. 2006 
Študent: Aleksander Vreže

Povzetek naloge:

Specifikacije realnih telekomunikacijskih sistemov v jeziku SDL so navadno obsežne, pravilnost delovanja pa je pogosto odvisna od časovnikov. V specifikacijah so lahko uporabljeni tudi zunanji gradniki, ki jih zaradi različnih razlogov pogosto ne moremo v celoti vključiti v model sistema. Zaradi navedenega se formalna verifikacija navadno izvaja samo nad izbranim delom specifikacije. Orodje Spin za formalno verifikacijo uporablja za opis modela jezik Promela, ki ne vključuje konstruktov za definicijo časovnikov in ne podpira racionalnih števil.

V disertaciji je podan nov model diskretnega časa za jezik Promela, algoritmi za avtomatsko vključevanje zunanjih gradnikov v jeziku C in algoritmi za uporabo racionalnih števil v jeziku Promela. Predstavljen je tudi mehanizem za abstrakcijo zunanjih gradnikov in postopek modeliranja procedur.

Teoretične raziskave smo podkrepili z implementacijo podanih algoritmov v jeziku C++. Algoritme smo vključili v orodje sdl2pml, ki ga uporabljamo za avtomatsko tvorbo modelov iz SDL-specifikacij. Delovanje algoritmov smo preverili s tvorbo modela specifikacije signalizacijskega protokola IUA, ki je uporabljen v elementih omrežja naslednje generacije. Praktičen del raziskav pokaže uporabnost predstavljenih pristopov in izpostavi nove izzive za prihodnje raziskovalno delo na področju avtomatske tvorbe modelov.