Metode preverjanja pravilnosti sistemov, ki temeljijo na testiranju, so se pri sodobnih kompleksnih sistemih izkazale kot zelo potratne, ker preverjanje dovolj velikega števila možnih izvajanj traja nesprejemljivo dolgo, v sistemih s sočasnostjo pa je pogosto tudi neobvladljivo in nepregledno. Pozno odkritje napake v programski opremi je zelo neugodno in drago. Za konkurenčnost podjetja na tržišču je zelo pomembno, da je le-to sposobno v relativno kratkem času razviti nov produkt. To pa je mogoče le, če že v fazi zasnove sistema odkrijemo čimveč pomanjkljivosti in napak. Za doseganje tega cilja potrebujemo učinkovite avtomatske metode verifikacije.

V okviru Centra odličnosti Informacijske in komunikacijske tehnologije smo izvedli projekt Verifikacija pravilnosti delovanja komunikacijskih sistemov. Cilj projekta je bil pridobivanje novega znanja na področju verifikacije komunikacijskih sistemov s poudarkom na razvoju idej v uporabno obliko in možnostih uporabe obetajočih rezultatov v industriji. Tako smo v okviru projekta za testni primer izbrali obsežni del programske kode v realnem produktu partnerja v projektu, podjetja Iskratel d.o.o. Koda je bila napisana v jeziku SDL in imela vključene konstrukte v jeziku C. Izvedli smo avtomatično pretvorbo te kode v model, opisan v jeziku Promela. Z orodjem Spin smo dobljeni model analizirali s simulacijo in pristopili k njegovi formalni verifikaciji.