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. |