Integracija orodja Spin v razvojno okolje Eclipse

Slovenski naslov:

Integracija orodja Spin v razvojno okolje Eclipse

Angleški naslov:

Integration of Spin tool into integrateddevelopment environment Eclipse

Študijski program:

Univerzitetni študijski program Telekomunikacije

Diplomski predmet:

Snovanje TK programske opreme

Mentor:

doc. dr. Boštjan Vlaovič

Komentor:

asist. dr. Aleksander Vreže

Povzetek:

Pri razvoju sistemov v telekomunikacijah se vedno več pozornosti namenja programski opremi. Preverjanje pravilnosti delovanja sistemov s sočasnostjo ni trivialno. Pri tem si lahko pomagamo z uporabo formalne verifikacije. V okviru diplomskega dela smo želeli povečati učinkovitost razvojnega inženirja in izboljšati uporabniško izkušnjo pri uporabi orodja za formalno verifikacijo Spin (Simple Promela Interpreter). Potreba po boljšem razvojnem okolju se je pojavila ob delu z velikimi modeli, ki so temeljili na industrijskih specifikacijah. Orodje Spin smo integrirali v razvojno okolje Eclipse z vtičnikom. Z barvanjem in krčenjem izvorne kode smo zagotovili preglednejše delo z večjimi modeli. Uporabniku ob urejanju kode dodatno pomagamo s prikazom rezerviranih besed in pregledom sintaktične pravilnosti modela. Omogočili smo uvoz in izvoz parametrov ter zagon simulacije in formalne verifikacije. V primeru, da model ne zadosti specifikaciji zahtev, je na voljo natančna pot izvajanja, ki je privedla do napake. V sistemih s sočasnostjo analiza vzrokov napake pogosto ni trivialna. Zato smo razvili algoritem za avtomatsko tvorbo diagramov MSC (Message Sequence Chart) iz sledi izvajanja. S tem smo pridobili standardiziran zapis, ki ga lahko urejamo tako v tekstovnih urejevalnikih kot v razvojnih orodjih,ki se uporabljajo na področju razvoja programske opreme v telekomunikacijah.