Izbor
Integracija orodja Spin v razvojno okolje Eclipse
Razpisana: 28. 11. 2005 Dodeljena: Zagovarjana: Študent: Raziskovalec: Aleksander Vreže, dr. Boštjan Vlaovič
Opis naloge:
| Orodje Spin je programski paket, ki se uporablja za načrtovanje in formalno verifikacijo asinhronih sistemov s sočasnostjo. Sistem opišemo v jeziku Promela. Opisan model sistema predstavlja vhod v orodje Spin. Z orodjem lahko izvajamo simulacijo ali formalno verifikacijo. Pri uporabi simulacije se lahko izvede naključna, vodena ali interaktivna simulacija sistema. Orodje je implementirano v jeziku ANSI C, zato ga je mogoče uporabiti na različnih operacijskih sistemih. Uporabljamo ga lahko v tekstovnem ali grafičnem načinu. Delo v tekstovnem načinu je manj pregledno, vendar je za izkušenega uporabnika veliko hitrejše. Grafični vmesnik XSpin je implementiran v jeziku Tcl/Tk in deluje neodvisno od orodja Spin. Delo s pomočjo grafičnega vmesnika je bolj zamudno, vendar je za uporabnika, ki si s tem orodjem pridobiva prve izkušnje, dobrodošlo. Grafični vmesnik uporabniku omogoča hitrejše razumevanje delovanja orodja. Trenutna implemetacija grafičnega vmesnika ima nekatere omejitve, ki so izrazitejše pri formalni verifikaciji večjih modelov (vzrok za omejitve je skriptni jezik Tcl/Tk). V okviru tega diplomskega dela se bo razvil vtič (plug-in) za orodje Eclipse, ki bo omogočal uporabo orodja Spin v orodju Eclipse. Pri tem bo potrebno implementirati vse funkcionalnosti, ki jih omogoča grafično orodje XSpin (nastavitev vhodnih parametrov, sledenje izvajanju simulacije, izris MSC-jev, izvoz MSC-jev v različne formate zapisa itd.). |
Zaželjena znanja: C++, Java
Formalna verifikacija telekomunikacijskih sistemov
V okviru Laboratorija za mikroračunalniške sisteme se raziskovalno ukvarjamo s formalno verifikacijo telekomunikacijskih sistemov s poudarkom na verifikaciji protokolov. V okviru diplomskih, magistrskih in doktorskih del smo pod mentorstvom red. prof. dr. Zmaga Brezočnika in izr. prof. dr. Tatjane Kapus razvili več programskih orodij. Delo na tem področju ni nikoli v celoti zaključeno, zato vas vabimo, da s svojim diplomskim delom prispevate k uresničitvi zastavljenih ciljev.
Od kandidata se ne pričakuje znanje s področja formalne verifikacije, pričakuje pa se pozitiven odnos do dela in želja po osvajanju novih znanj s področja razvoja programske opreme. Delo bo orientirano aplikativno s končnim ciljem razvoja dela okolja za formalno verifikacijo protokolov v telekomunikacijah, ki bo uporabno tudi za industrijske potrebe. Po opravljenem diplomskem delu nudimo možnost nadaljevanja študija v okviru razpisanih tem za magistrski in doktorski študij. Možen je tudi dogovor o zaposlitvi v okviru programa mladi raziskovalci.
Razvojno delo bo potekalo v sodelovanju s podiplomskimi študenti in raziskovalci na zmogljivem 64-bitnem strežniku pod operacijskim sistemom Linux. Za razvojno okolje smo izbrali Eclipse, ki ...
Zainteresirani kandidati naj pošljejo e-sporočilo na naslov bostjan.vlaovic[AT]uni-mb.si ali pokličejo na telefon +386 2 220 7217 (dr. Boštjan Vlaovič).
