28. 11. 2005

doktorske disertacije

V nadaljevanju podajamo področja raziskav, ki bi bistveno prispevala k uporabi formalne verifikacije v telekomunikacijski industriji. Konkretnih tem za doktorske disertacije zaradi neraziskanosti predlaganih področij ni mogoče definirati vnaprej, saj je najprej potrebno oceniti znanstveni prispevek rešitve posameznega problema. V nadaljevanju zato podajamo seznam aktualnih problemov pri formalni verifikaciji specifikacij v jeziku SDL z avtomatsko tvorbo modelov v jeziku Promela in uporabo orodja Spin:

Podpora tabelam pri definiciji kanalov v jeziku Promela in dopolnitev algoritmov za tvorbo verifikatorja orodja Spin

Orodje Spin in jezik Promela ne podpirata ...
Orodje Spin ob tvorbi verifikatorja v jeziku C ...
V okviru naloge "Avtomatska tvorba modelov s sondami iz specifikacije sistema v jeziku SDL" smo kot prvi podprli dinamično tvorbo procesov z reciklažo pridruženih identifikacijskih številk. Ta omogoča minimalno porabo pomnilniškega prostora za spremljanje pridružene vhodne vrste. Pri tem smo naleteli na omejitve, ki jih postavlja semantika jezika Promela. Ta razlikuje med terminacijo in ubitjem procesa, kjer terminacija označuje zaključek izvajanja, ubitje pa sprostitev pridružene identifikacijske številke. Nabor specifikacij, ki jih lahko preverimo v celoti, je zato omejen na tiste, kjer se procesi tvorijo in ubijajo v obratnem vrstnem redu. Razširitev orodja Spin z dosledno podporo semantičnim pravilom jezika Promela lahko te težave delno odpravi. Kljub temu takšen model vsebuje veliko število virtualnih mogočih izvajalnih poti, ki močno povečajo časovno in prostorsko zahtevnost formalne verifikacije. Verifikacija teh specifikacij je zaradi uporabe tehnike ``on the fly'' vseeno mogoča.

Za odpravo teh omejitev je potrebno temeljito preučiti delovanje algoritmov za formalno formalno verifikacijo in jih dopolniti oz. nadomestiti s takšnimi, ki ne razlikujejo med terminacijo in ubitjem procesa.